diff options
| author | Gaëtan Gilbert | 2019-05-20 17:02:55 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 788b47d9dd70dc9f8057d4a9353ed24f091ea917 (patch) | |
| tree | 9fe8bc0a513e39f75b9e6697433af983bc695ee9 /vernac/vernacextend.ml | |
| parent | 445dee163b7a2c9d4cc24da739d743d80fcec529 (diff) | |
Vernacextend only returns a proof_global.t option, not a vernacstate
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 730f5fd6da..008d3d854f 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -53,14 +53,14 @@ type vernac_when = | VtLater type vernac_classification = vernac_type * vernac_when -type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.t option -> Proof_global.t option type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * (plugin_args -> vernac_command)) Hashtbl.t) let vinterp_add depr s f = try @@ -83,7 +83,7 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let call opn converted_args ~atts ~st = +let call opn converted_args ~atts ~pstate = let phase = ref "Looking up command" in try let depr, callback = vinterp_map opn in @@ -99,7 +99,7 @@ let call opn converted_args ~atts ~st = phase := "Checking arguments"; let hunk = callback converted_args in phase := "Executing command"; - hunk ~atts ~st + hunk ~atts ~pstate with | reraise -> let reraise = CErrors.push reraise in @@ -125,7 +125,7 @@ let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater type (_, _) ty_sig = -| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyNil : (vernac_command, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig @@ -151,7 +151,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio end (** Stupid GADTs forces us to duplicate the definition just for typing *) -let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_command = function | TyNil -> fun f args -> begin match args with | [] -> f |