Vernacextend only returns a proof_global.t option, not a vernacstate

4 files changed, 26 insertions, 30 deletions

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 ->