aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml2
-rw-r--r--dev/top_printers.ml4
-rw-r--r--vernac/vernacentries.ml33
-rw-r--r--vernac/vernacentries.mli5
-rw-r--r--vernac/vernacextend.ml12
-rw-r--r--vernac/vernacextend.mli6
6 files changed, 29 insertions, 33 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index ad79599cf4..b118d9ec00 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -384,7 +384,7 @@ let print_body_fun state fmt r =
print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_wrapper state) r
let print_body state fmt r =
- fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]"
+ fprintf fmt "@[(%afun %a~atts@ ~pstate@ -> coqpp_body %a%a ~pstate)@]"
(print_body_fun state) r print_binders r.vernac_toks
print_binders r.vernac_toks print_atts_right r.vernac_atts
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 2859b56cbe..db444a9b78 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -532,7 +532,7 @@ let _ =
let open Vernacextend 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 ~atts ~st = in_current_context econstr_display c; st in
+ let cmd_fn c ~atts ~pstate = in_current_context econstr_display c; pstate in
let cmd_class _ = VtQuery,VtNow in
let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
vernac_extend ~command:"PrintConstr" [cmd]
@@ -541,7 +541,7 @@ let _ =
let open Vernacextend 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 ~atts ~st = in_current_context print_pure_econstr c; st in
+ let cmd_fn c ~atts ~pstate = in_current_context print_pure_econstr c; pstate in
let cmd_class _ = VtQuery,VtNow in
let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
vernac_extend ~command:"PrintPureConstr" [cmd]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e4667e376c..49ce27ee30 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2629,9 +2629,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
(* Extensions *)
| VernacExtend (opn,args) ->
- (* XXX: Here we are returning the state! :) *)
- let st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
- st.Vernacstate.proof
+ Vernacextend.call ~atts opn args ~pstate
(* XXX: This won't properly set the proof mode, as of today, it is
controlled by the STM. Thus, we would need access information from
@@ -2723,27 +2721,22 @@ type functional_vernac =
| VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
| VtReadProof of (pstate:Proof_global.pstate -> unit)
-let interp_functional_vernac c ~st =
+let interp_functional_vernac c ~pstate =
let open Proof_global in
- let open Vernacstate in
match c with
- | VtDefault f -> f (); st
- | VtModifyProofStack f ->
- let proof = f ~pstate:st.proof in { st with proof }
+ | VtDefault f -> f (); pstate
+ | VtModifyProofStack f -> f ~pstate
| VtMaybeOpenProof f ->
- let pstate = f () in
- let proof = maybe_push ~ontop:st.proof pstate in
- { st with proof }
+ let proof = f () in
+ let pstate = maybe_push ~ontop:pstate proof in
+ pstate
| VtOpenProof f ->
- let pstate = f () in
- let proof = Some (push ~ontop:st.proof pstate) in
- { st with proof }
+ Some (push ~ontop:pstate (f ()))
| VtModifyProof f ->
- let proof = modify_pstate f ~pstate:st.proof in
- { st with proof }
+ modify_pstate f ~pstate
| VtReadProofOpt f ->
- f ~pstate:(Option.map get_current_pstate st.proof);
- st
+ f ~pstate:(Option.map get_current_pstate pstate);
+ pstate
| VtReadProof f ->
- with_pstate ~pstate:st.proof f;
- st
+ with_pstate ~pstate f;
+ pstate
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 9756c1e0bb..55763d9e51 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -63,4 +63,7 @@ type functional_vernac =
| VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
| VtReadProof of (pstate:Proof_global.pstate -> unit)
-val interp_functional_vernac : functional_vernac -> st:Vernacstate.t -> Vernacstate.t
+val interp_functional_vernac
+ : functional_vernac
+ -> pstate:Proof_global.t option
+ -> Proof_global.t option
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
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index b37e527f47..6189830929 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -71,18 +71,18 @@ type vernac_classification = vernac_type * vernac_when
(** Interpretation of extended vernac phrases. *)
-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
-val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> vernac_command
(** {5 VERNAC EXTEND} *)
type classifier = Genarg.raw_generic_argument list -> vernac_classification
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 ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:31:07 +0000