From 349ed92929a6199b6b3eccfddb6ffb9f7914897c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 5 Jul 2023 16:14:18 +0200 Subject: [PATCH] Move typed_vernac to its own file from vernacextend --- coqpp/coqpp_main.ml | 4 +- .../17818-SkySkimmer-vernactypes.sh | 3 + dev/top_printers.ml | 2 + plugins/funind/g_indfun.mlg | 4 +- vernac/synterp.ml | 2 +- vernac/synterp.mli | 2 +- vernac/vernacentries.ml | 12 +- vernac/vernacentries.mli | 2 +- vernac/vernacextend.ml | 145 +---------------- vernac/vernacextend.mli | 72 +-------- vernac/vernacinterp.ml | 4 +- vernac/vernactypes.ml | 153 ++++++++++++++++++ vernac/vernactypes.mli | 78 +++++++++ 13 files changed, 253 insertions(+), 230 deletions(-) create mode 100644 dev/ci/user-overlays/17818-SkySkimmer-vernactypes.sh create mode 100644 vernac/vernactypes.ml create mode 100644 vernac/vernactypes.mli diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 0e8313a57341..398f67545728 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -410,11 +410,11 @@ let pr_end_wrapper fmt = function let print_body_state state fmt r = let state = match r.vernac_state with Some _ as s -> s | None -> state in match state with - | None -> fprintf fmt "Vernacextend.vtdefault (fun () -> %a)" print_code r.vernac_body + | None -> fprintf fmt "Vernactypes.vtdefault (fun () -> %a)" print_code r.vernac_body | Some "CUSTOM" -> print_code fmt r.vernac_body | Some state -> let state, wrap = understand_state state in - fprintf fmt "Vernacextend.%s (%a (%a)%a)" state pr_begin_wrapper wrap + fprintf fmt "Vernactypes.%s (%a (%a)%a)" state pr_begin_wrapper wrap print_code r.vernac_body pr_end_wrapper wrap let print_body_fun state fmt r = diff --git a/dev/ci/user-overlays/17818-SkySkimmer-vernactypes.sh b/dev/ci/user-overlays/17818-SkySkimmer-vernactypes.sh new file mode 100644 index 000000000000..0da0043cea2e --- /dev/null +++ b/dev/ci/user-overlays/17818-SkySkimmer-vernactypes.sh @@ -0,0 +1,3 @@ +overlay tactician https://github.com/SkySkimmer/coq-tactician vernactypes 17818 + +overlay elpi https://github.com/SkySkimmer/coq-elpi vernactypes 17818 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 60f583ea61bf..079d526cc77c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -614,6 +614,7 @@ END let () = let open Vernacextend in + let open Vernactypes in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context econstr_display c) in @@ -623,6 +624,7 @@ let () = let () = let open Vernacextend in + let open Vernactypes in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context print_pure_econstr c) in diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index be137de96e1d..f6d9a0c92076 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -211,11 +211,11 @@ VERNAC COMMAND EXTEND Function STATE CUSTOM -> { let warn = "-unused-pattern-matching-variable,-non-recursive" in if is_interactive recsl then - Vernacextend.vtopenproof (fun () -> + Vernactypes.vtopenproof (fun () -> CWarnings.with_warn warn Gen_principle.do_generate_principle_interactive (List.map snd recsl)) else - Vernacextend.vtdefault (fun () -> + Vernactypes.vtdefault (fun () -> CWarnings.with_warn warn Gen_principle.do_generate_principle (List.map snd recsl)) } diff --git a/vernac/synterp.ml b/vernac/synterp.ml index 41b3cff19fab..b28e1ee21129 100644 --- a/vernac/synterp.ml +++ b/vernac/synterp.ml @@ -108,7 +108,7 @@ type synterp_entry = | EVernacInclude of Declaremods.module_expr list | EVernacSetOption of { export : bool; key : Goptions.option_name; value : Vernacexpr.option_setting } | EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list - | EVernacExtend of Vernacextend.typed_vernac + | EVernacExtend of Vernactypes.typed_vernac and vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen diff --git a/vernac/synterp.mli b/vernac/synterp.mli index e20e04172c2e..fbdd5bdc7a89 100644 --- a/vernac/synterp.mli +++ b/vernac/synterp.mli @@ -60,7 +60,7 @@ type synterp_entry = | EVernacInclude of Declaremods.module_expr list | EVernacSetOption of { export : bool; key : Goptions.option_name; value : Vernacexpr.option_setting } | EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list - | EVernacExtend of Vernacextend.typed_vernac + | EVernacExtend of Vernactypes.typed_vernac and vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43d07ce5bf57..55a30b1719e4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1368,7 +1368,7 @@ let vernac_end_segment ~pm ~proof ({v=id} as lid) = | _ -> assert false let vernac_end_segment lid = - Vernacextend.TypedVernac { + Vernactypes.TypedVernac { inprog = Use; outprog = Pop; inproof = UseOpt; outproof = No; run = (fun ~pm ~proof -> let () = vernac_end_segment ~pm ~proof lid in @@ -1376,9 +1376,9 @@ let vernac_end_segment lid = } let vernac_begin_segment ~interactive f = - let inproof = Vernacextend.InProof.(if interactive then Reject else Ignore) in - let outprog = Vernacextend.OutProg.(if interactive then Push else No) in - Vernacextend.TypedVernac { + let inproof = Vernactypes.InProof.(if interactive then Reject else Ignore) in + let outprog = Vernactypes.OutProg.(if interactive then Push else No) in + Vernactypes.TypedVernac { inprog = Ignore; outprog; inproof; outproof = No; run = (fun ~pm ~proof -> let () = f () in @@ -2213,7 +2213,7 @@ let vernac_validate_proof ~pstate = str "No issues found." else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues) -let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with +let translate_vernac_synterp ?loc ~atts v = let open Vernactypes in match v with | EVernacNotation { local; decl } -> vtdefault(fun () -> Metasyntax.add_notation_interpretation ~local (Global.env()) decl) @@ -2273,7 +2273,7 @@ let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v wit (* Extensions *) | EVernacExtend f -> f -let translate_pure_vernac ?loc ~atts v = let open Vernacextend in match v with +let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with | VernacAbortAll | VernacRestart | VernacUndo _ diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 7ff2d2db427a..cc92c982f124 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -20,7 +20,7 @@ val translate_vernac : ?loc:Loc.t -> atts:Attributes.vernac_flags -> Synterp.vernac_entry - -> Vernacextend.typed_vernac + -> Vernactypes.typed_vernac (** Vernacular require command, used by the command line *) val vernac_require diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e1ccf8b2bd03..f0d235002ee1 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -11,6 +11,7 @@ open Util open Pp open CErrors +open Vernactypes type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque @@ -51,150 +52,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *) and proof_block_name = string (** open type of delimiters *) -module InProg = struct - type _ t = - | Ignore : unit t - | Use : Declare.OblState.t t - - let cast (type a) (x:Declare.OblState.t) (ty:a t) : a = - match ty with - | Ignore -> () - | Use -> x -end - -module OutProg = struct - type _ t = - | No : unit t - | Yes : Declare.OblState.t t - | Push - | Pop - - let cast (type a) (x:a) (ty:a t) (orig:Declare.OblState.t NeList.t) : Declare.OblState.t NeList.t = - match ty with - | No -> orig - | Yes -> NeList.map_head (fun _ -> x) orig - | Push -> NeList.push Declare.OblState.empty (Some orig) - | Pop -> (match NeList.tail orig with Some tl -> tl | None -> assert false) -end - -module InProof = struct - type _ t = - | Ignore : unit t - | Reject : unit t - | Use : Declare.Proof.t t - | UseOpt : Declare.Proof.t option t - - let cast (type a) (x:Declare.Proof.t option) (ty:a t) : a = - match x, ty with - | _, Ignore -> () - | None, Reject -> () - | Some _, Reject -> CErrors.user_err (Pp.str "Command not supported (Open proofs remain).") - | Some x, Use -> x - | None, Use -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).") - | _, UseOpt -> x -end - -module OutProof = struct - type _ t = - | No : unit t - | Close : unit t - | Update : Declare.Proof.t t - | New : Declare.Proof.t t - -end - -type ('inprog,'outprog,'inproof,'outproof) vernac_type = { - inprog : 'inprog InProg.t; - outprog : 'outprog InProg.t; - inproof : 'inproof InProof.t; - outproof : 'outproof OutProof.t; -} - -type typed_vernac = - TypedVernac : { - inprog : 'inprog InProg.t; - outprog : 'outprog OutProg.t; - inproof : 'inproof InProof.t; - outproof : 'outproof OutProof.t; - run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof; - } -> typed_vernac - -let vtdefault f = - TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No; - run = (fun ~pm:() ~proof:() -> - let () = f () in - (), ()) } - -let vtnoproof f = - TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No; - run = (fun ~pm:() ~proof:() -> - let () = f () in - (), ()) - } - -let vtcloseproof f = - TypedVernac { inprog = Use; outprog = Yes; inproof = Use; outproof = Close; - run = (fun ~pm ~proof -> - let pm = f ~lemma:proof ~pm in - pm, ()) - } - -let vtopenproof f = - TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = New; - run = (fun ~pm:() ~proof:() -> - let proof = f () in - (), proof) - } - -let vtmodifyproof f = - TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = Update; - run = (fun ~pm:() ~proof -> - let proof = f ~pstate:proof in - (), proof) - } - -let vtreadproofopt f = - TypedVernac { inprog = Ignore; outprog = No; inproof = UseOpt; outproof = No; - run = (fun ~pm:() ~proof -> - let () = f ~pstate:proof in - (), ()) - } - -let vtreadproof f = - TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = No; - run = (fun ~pm:() ~proof -> - let () = f ~pstate:proof in - (), ()) - } - -let vtreadprogram f = - TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = No; - run = (fun ~pm ~proof:() -> - let () = f ~pm in - (), ()) - } - -let vtmodifyprogram f = - TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = No; - run = (fun ~pm ~proof:() -> - let pm = f ~pm in - pm, ()) - } - -let vtdeclareprogram f = - TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = New; - run = (fun ~pm ~proof:() -> - let proof = f ~pm in - (), proof) - } - -let vtopenproofprogram f = - TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = New; - run = (fun ~pm ~proof:() -> - let pm, proof = f ~pm in - pm, proof) - } - type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac type plugin_args = Genarg.raw_generic_argument list diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4c2a3dba5bbe..ab7241b12dfc 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -67,77 +67,7 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *) and proof_block_name = string (** open type of delimiters *) -(** Interpretation of extended vernac phrases. *) - -module InProg : sig - type _ t = - | Ignore : unit t - | Use : Declare.OblState.t t - - val cast : Declare.OblState.t -> 'a t -> 'a -end - -module OutProg : sig - type _ t = - | No : unit t - | Yes : Declare.OblState.t t - | Push - | Pop - - val cast : 'a -> 'a t -> Declare.OblState.t NeList.t -> Declare.OblState.t NeList.t -end - -module InProof : sig - type _ t = - | Ignore : unit t - | Reject : unit t - | Use : Declare.Proof.t t - | UseOpt : Declare.Proof.t option t - - val cast : Declare.Proof.t option -> 'a t -> 'a -end - -module OutProof : sig - - type _ t = - | No : unit t - | Close : unit t - | Update : Declare.Proof.t t - | New : Declare.Proof.t t - -end - -type ('inprog,'outprog,'inproof,'outproof) vernac_type = { - inprog : 'inprog InProg.t; - outprog : 'outprog InProg.t; - inproof : 'inproof InProof.t; - outproof : 'outproof OutProof.t; -} - -type typed_vernac = - TypedVernac : { - inprog : 'inprog InProg.t; - outprog : 'outprog OutProg.t; - inproof : 'inproof InProof.t; - outproof : 'outproof OutProof.t; - run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof; - } -> typed_vernac - -(** Some convenient typed_vernac constructors. Keep in sync with coqpp. *) - -val vtdefault : (unit -> unit) -> typed_vernac -val vtnoproof : (unit -> unit) -> typed_vernac -val vtcloseproof : (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac -val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac -val vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac -val vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac -val vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac -val vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac -val vtmodifyprogram : (pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac -val vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac -val vtopenproofprogram : (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -> typed_vernac - -type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac +type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> Vernactypes.typed_vernac type plugin_args = Genarg.raw_generic_argument list diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 95de8025fa78..694d62e27711 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -13,9 +13,9 @@ open Synterp let vernac_pperr_endline = CDebug.create ~name:"vernacinterp" () -let interp_typed_vernac (Vernacextend.TypedVernac { inprog; outprog; inproof; outproof; run }) +let interp_typed_vernac (Vernactypes.TypedVernac { inprog; outprog; inproof; outproof; run }) ~pm ~stack = - let open Vernacextend in + let open Vernactypes in let module LStack = Vernacstate.LemmaStack in let proof = Option.map LStack.get_top stack in let pm', proof' = run diff --git a/vernac/vernactypes.ml b/vernac/vernactypes.ml new file mode 100644 index 000000000000..fc9580b4a39a --- /dev/null +++ b/vernac/vernactypes.ml @@ -0,0 +1,153 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* () + | Use -> x +end + +module OutProg = struct + type _ t = + | No : unit t + | Yes : Declare.OblState.t t + | Push + | Pop + + let cast (type a) (x:a) (ty:a t) (orig:Declare.OblState.t NeList.t) : Declare.OblState.t NeList.t = + match ty with + | No -> orig + | Yes -> NeList.map_head (fun _ -> x) orig + | Push -> NeList.push Declare.OblState.empty (Some orig) + | Pop -> (match NeList.tail orig with Some tl -> tl | None -> assert false) +end + +module InProof = struct + type _ t = + | Ignore : unit t + | Reject : unit t + | Use : Declare.Proof.t t + | UseOpt : Declare.Proof.t option t + + let cast (type a) (x:Declare.Proof.t option) (ty:a t) : a = + match x, ty with + | _, Ignore -> () + | None, Reject -> () + | Some _, Reject -> CErrors.user_err (Pp.str "Command not supported (Open proofs remain).") + | Some x, Use -> x + | None, Use -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).") + | _, UseOpt -> x +end + +module OutProof = struct + type _ t = + | No : unit t + | Close : unit t + | Update : Declare.Proof.t t + | New : Declare.Proof.t t + +end + +type ('inprog,'outprog,'inproof,'outproof) vernac_type = { + inprog : 'inprog InProg.t; + outprog : 'outprog InProg.t; + inproof : 'inproof InProof.t; + outproof : 'outproof OutProof.t; +} + +type typed_vernac = + TypedVernac : { + inprog : 'inprog InProg.t; + outprog : 'outprog OutProg.t; + inproof : 'inproof InProof.t; + outproof : 'outproof OutProof.t; + run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof; + } -> typed_vernac + +let vtdefault f = + TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No; + run = (fun ~pm:() ~proof:() -> + let () = f () in + (), ()) } + +let vtnoproof f = + TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No; + run = (fun ~pm:() ~proof:() -> + let () = f () in + (), ()) + } + +let vtcloseproof f = + TypedVernac { inprog = Use; outprog = Yes; inproof = Use; outproof = Close; + run = (fun ~pm ~proof -> + let pm = f ~lemma:proof ~pm in + pm, ()) + } + +let vtopenproof f = + TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = New; + run = (fun ~pm:() ~proof:() -> + let proof = f () in + (), proof) + } + +let vtmodifyproof f = + TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = Update; + run = (fun ~pm:() ~proof -> + let proof = f ~pstate:proof in + (), proof) + } + +let vtreadproofopt f = + TypedVernac { inprog = Ignore; outprog = No; inproof = UseOpt; outproof = No; + run = (fun ~pm:() ~proof -> + let () = f ~pstate:proof in + (), ()) + } + +let vtreadproof f = + TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = No; + run = (fun ~pm:() ~proof -> + let () = f ~pstate:proof in + (), ()) + } + +let vtreadprogram f = + TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = No; + run = (fun ~pm ~proof:() -> + let () = f ~pm in + (), ()) + } + +let vtmodifyprogram f = + TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = No; + run = (fun ~pm ~proof:() -> + let pm = f ~pm in + pm, ()) + } + +let vtdeclareprogram f = + TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = New; + run = (fun ~pm ~proof:() -> + let proof = f ~pm in + (), proof) + } + +let vtopenproofprogram f = + TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = New; + run = (fun ~pm ~proof:() -> + let pm, proof = f ~pm in + pm, proof) + } diff --git a/vernac/vernactypes.mli b/vernac/vernactypes.mli new file mode 100644 index 000000000000..5b0ca0c76d81 --- /dev/null +++ b/vernac/vernactypes.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 'a t -> 'a +end + +module OutProg : sig + type _ t = + | No : unit t + | Yes : Declare.OblState.t t + | Push + | Pop + + val cast : 'a -> 'a t -> Declare.OblState.t NeList.t -> Declare.OblState.t NeList.t +end + +module InProof : sig + type _ t = + | Ignore : unit t + | Reject : unit t + | Use : Declare.Proof.t t + | UseOpt : Declare.Proof.t option t + + val cast : Declare.Proof.t option -> 'a t -> 'a +end + +module OutProof : sig + + type _ t = + | No : unit t + | Close : unit t + | Update : Declare.Proof.t t + | New : Declare.Proof.t t + +end + +type ('inprog,'outprog,'inproof,'outproof) vernac_type = { + inprog : 'inprog InProg.t; + outprog : 'outprog InProg.t; + inproof : 'inproof InProof.t; + outproof : 'outproof OutProof.t; +} + +type typed_vernac = + TypedVernac : { + inprog : 'inprog InProg.t; + outprog : 'outprog OutProg.t; + inproof : 'inproof InProof.t; + outproof : 'outproof OutProof.t; + run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof; + } -> typed_vernac + +(** Some convenient typed_vernac constructors. Used by coqpp. *) + +val vtdefault : (unit -> unit) -> typed_vernac +val vtnoproof : (unit -> unit) -> typed_vernac +val vtcloseproof : (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac +val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac +val vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac +val vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac +val vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac +val vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac +val vtmodifyprogram : (pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac +val vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac +val vtopenproofprogram : (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -> typed_vernac