21 files changed, 76 insertions, 76 deletions

diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 6e4bffa0b6..6bb923118e 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -12,4 +12,4 @@
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate
+val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index efd5b5575f..7d04fee7c1 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
 
 (* Show the extraction of the current ongoing proof *)
 
-val show_extraction : pstate:Proof_global.pstate -> unit
+val show_extraction : pstate:Proof_global.t -> unit
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 16df34e214..7c6669d0fc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -634,7 +634,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   
 
 let do_generate_principle pconstants on_error register_built interactive_proof
-    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate option =
+    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let pstate, _is_struct =
     match fixpoint_exprl with
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index cd39266378..47d37b29a5 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -8,7 +8,7 @@ val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val do_generate_principle :
   bool ->
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Proof_global.pstate option
+  Proof_global.t option
 
 val functional_induction :
   bool ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b4d0f092d8..5a682e7231 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1495,7 +1495,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
-    generate_induction_principle using_lemmas : Proof_global.pstate option =
+    generate_induction_principle using_lemmas : Proof_global.t option =
   let open Term in
   let open Constr in
   let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 84d7a399e1..90f9c449b1 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,4 +14,4 @@ bool ->
            int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
             pconstant ->
-            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5d57a2f27f..26d477fee0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1973,7 +1973,7 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer atts m n : Proof_global.pstate option =
+let add_morphism_infer atts m n : Proof_global.t option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index e1cbc46b3b..5aabb946d5 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,7 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
 
 val add_morphism
   : rewrite_attributes
@@ -109,7 +109,7 @@ val add_morphism
   -> constr_expr
   -> constr_expr
   -> Id.t
-  -> Proof_global.pstate
+  -> Proof_global.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ec52d2d5cf..77d701b41f 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -23,17 +23,17 @@ exception NoSuchGoal
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
-val get_goal_context : Proof_global.pstate -> int -> Evd.evar_map * env
+val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
 
 (** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof_global.pstate -> Evd.evar_map * env
+val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
 
 (** [get_current_context ()] returns the context of the
   current focused goal. If there is no focused goal but there
   is a proof in progress, it returns the corresponding evar_map.
   If there is no pending proof then it returns the current global
   environment and empty evar_map. *)
-val get_current_context : Proof_global.pstate -> Evd.evar_map * env
+val get_current_context : Proof_global.t -> Evd.evar_map * env
 
 (** {6 ... } *)
 
@@ -49,7 +49,7 @@ val solve : ?with_end_tac:unit Proofview.tactic ->
     focused proof.
     Returns [false] if an unsafe tactic has been used. *)
 
-val by : unit Proofview.tactic -> Proof_global.pstate -> Proof_global.pstate * bool
+val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
 
 (** Option telling if unification heuristics should be used. *)
 val use_unification_heuristics : unit -> bool
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e26577e8bd..b642e8eea7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -45,7 +45,7 @@ type proof_ending =
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
-type pstate = {
+type t = {
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Constr.named_context option;
@@ -56,7 +56,7 @@ type pstate = {
 
 (* The head of [t] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
-type stack = pstate * pstate list
+type stack = t * t list
 
 let pstate_map f (pf, pfl) = (f pf, List.map f pfl)
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index aa538bd581..aff48b9636 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -12,20 +12,20 @@
      toplevel. In particular it defines the global proof
      environment. *)
 
-type pstate
+type t
 type stack
 
-val get_current_pstate : stack -> pstate
+val get_current_pstate : stack -> t
 
-val get_current_proof_name : pstate -> Names.Id.t
-val get_current_persistence : pstate -> Decl_kinds.goal_kind
+val get_current_proof_name : t -> Names.Id.t
+val get_current_persistence : t -> Decl_kinds.goal_kind
 val get_all_proof_names : stack -> Names.Id.t list
 
 val discard : Names.lident -> stack -> stack option
 val discard_current : stack -> stack option
 
-val give_me_the_proof : pstate -> Proof.t
-val compact_the_proof : pstate -> pstate
+val give_me_the_proof : t -> Proof.t
+val compact_the_proof : t -> t
 
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
@@ -56,9 +56,9 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
-val push : ontop:stack option -> pstate -> stack
+val push : ontop:stack option -> t -> stack
 
-val maybe_push : ontop:stack option -> pstate option -> stack option
+val maybe_push : ontop:stack option -> t option -> stack option
 
 (** [start_proof ~ontop id str pl goals terminator] starts a proof of name
    [id] with goals [goals] (a list of pairs of environment and
@@ -71,23 +71,23 @@ val maybe_push : ontop:stack option -> pstate option -> stack option
 val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
-    proof_terminator -> pstate
+    proof_terminator -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
   Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
-  Proofview.telescope -> proof_terminator -> pstate
+  Proofview.telescope -> proof_terminator -> t
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
   there_are_pending_proofs. *)
-val update_global_env : pstate -> pstate
+val update_global_env : t -> t
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
 val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn ->
-  pstate -> closed_proof
+  t -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -97,15 +97,15 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> pstate -> closed_proof_output
-val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> pstate ->
+val return_proof : ?allow_partial:bool -> t -> closed_proof_output
+val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
   closed_proof_output Future.computation -> closed_proof
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-val get_terminator : pstate -> proof_terminator
-val set_terminator : proof_terminator -> pstate -> pstate
-val get_open_goals : pstate -> int
+val get_terminator : t -> proof_terminator
+val set_terminator : proof_terminator -> t -> t
+val get_open_goals : t -> int
 
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
     no current proof.
@@ -115,24 +115,24 @@ val with_current_proof :
 val simple_with_current_proof :
   (unit Proofview.tactic -> Proof.t -> Proof.t) -> stack -> stack
 
-val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> pstate -> pstate * 'a
-val modify_proof : (Proof.t -> Proof.t) -> pstate -> pstate
+val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+val modify_proof : (Proof.t -> Proof.t) -> t -> t
 
-val with_current_pstate : (pstate -> pstate * 'a) -> stack -> stack * 'a
-val modify_current_pstate : (pstate -> pstate) -> stack -> stack
+val with_current_pstate : (t -> t * 'a) -> stack -> stack * 'a
+val modify_current_pstate : (t -> t) -> stack -> stack
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Genarg.glob_generic_argument -> pstate -> pstate
+val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 
 (** Sets the section variables assumed by the proof, returns its closure
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
-val set_used_variables : pstate ->
-  Names.Id.t list -> (Constr.named_context * Names.lident list) * pstate
+val set_used_variables : t ->
+  Names.Id.t list -> (Constr.named_context * Names.lident list) * t
 
-val get_used_variables : pstate -> Constr.named_context option
+val get_used_variables : t -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : pstate -> UState.universe_decl
+val get_universe_decl : t -> UState.universe_decl
 
 val copy_terminators : src:stack -> tgt:stack -> stack
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 396c3e2fed..7b8f96cdd8 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -292,7 +292,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Proof_global.pstate -> Pp.t
+val pr_applicable_hint : Proof_global.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 273cf02c9b..80d48f67ba 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -29,7 +29,7 @@ val register_struct
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
 
-val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit
+val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
 
 (** {5 Notations} *)
 
@@ -51,7 +51,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Proof_global.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate
+val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
 
 (** {5 Toplevel exceptions} *)
 
diff --git a/vernac/classes.mli b/vernac/classes.mli
index d441fd342c..daba78217b 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -43,7 +43,7 @@ val new_instance :
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
-  -> Id.t * Proof_global.pstate option (* May open a proof *)
+  -> Id.t * Proof_global.t option (* May open a proof *)
 
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index d36593332e..9e376c8f96 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -20,11 +20,11 @@ open Vernacexpr
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.pstate option
+  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.pstate option
+  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
 
 (************************************************************************)
 (** Internal API  *)
@@ -85,14 +85,14 @@ val declare_fixpoint :
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list ->
-  Proof_global.pstate option
+  Proof_global.t option
 
 val declare_cofixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   decl_notation list ->
-  Proof_global.pstate option
+  Proof_global.t option
 
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index e613b79c7b..c4c609e824 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -41,13 +41,13 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map
   ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val ->
   ?compute_guard:Proof_global.lemma_possible_guards ->
-  ?hook:declaration_hook -> EConstr.types -> Proof_global.pstate
+  ?hook:declaration_hook -> EConstr.types -> Proof_global.t
 
 val start_proof_com
   :  program_mode:bool
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
-  -> Proof_global.pstate
+  -> Proof_global.t
 
 val start_proof_with_initialization :
   ?hook:declaration_hook ->
@@ -55,7 +55,7 @@ val start_proof_with_initialization :
   (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t (* name of thm *) *
      (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-  -> int list option -> Proof_global.pstate
+  -> int list option -> Proof_global.t
 
 val standard_proof_terminator :
   ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
@@ -72,7 +72,7 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 val save_proof_admitted
   :  ?proof:Proof_global.closed_proof
-  -> pstate:Proof_global.pstate
+  -> pstate:Proof_global.t
   -> unit
 
 val save_proof_proved
@@ -83,7 +83,7 @@ val save_proof_proved
   -> Proof_global.stack option
 
 val save_pstate_proved
-  : pstate:Proof_global.pstate
+  : pstate:Proof_global.t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 7db094a75d..3b77039de5 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -88,12 +88,12 @@ val add_mutual_definitions :
 val obligation
   : int * Names.Id.t option * Constrexpr.constr_expr option
   -> Genarg.glob_generic_argument option
-  -> Proof_global.pstate
+  -> Proof_global.t
 
 val next_obligation
   : Names.Id.t option
   -> Genarg.glob_generic_argument option
-  -> Proof_global.pstate
+  -> Proof_global.t
 
 val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)
diff --git a/vernac/search.mli b/vernac/search.mli
index f8074a67ff..0f94ddc5b6 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -39,13 +39,13 @@ val search_about_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_rewrite : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_pattern : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_about   : ?pstate:Proof_global.pstate -> int option -> (bool * glob_search_about_item) list
+val search_about   : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
@@ -66,12 +66,12 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : ?pstate:Proof_global.pstate -> ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list ->
   constr coq_object list
 
 (** {6 Generic search function} *)
 
-val generic_search : ?pstate:Proof_global.pstate -> int option -> display_function -> unit
+val generic_search : ?pstate:Proof_global.t -> int option -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8d15191ebe..c88de1181a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1114,7 +1114,7 @@ let vernac_set_end_tac ~pstate tac =
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
   Proof_global.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~(pstate : Proof_global.pstate) e : Proof_global.pstate =
+let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
   let env = Global.env () in
   let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
   let tys =
@@ -2715,11 +2715,11 @@ let interp ?(verbosely=true) ?proof ~st cmd =
 type functional_vernac =
   | VtDefault of (unit -> unit)
   | VtModifyProofStack of (pstate:Proof_global.stack option -> Proof_global.stack option)
-  | VtMaybeOpenProof of (unit -> Proof_global.pstate option)
-  | VtOpenProof of (unit -> Proof_global.pstate)
-  | VtModifyProof of (pstate:Proof_global.pstate -> Proof_global.pstate)
-  | VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
-  | VtReadProof of (pstate:Proof_global.pstate -> unit)
+  | VtMaybeOpenProof of (unit -> Proof_global.t option)
+  | VtOpenProof of (unit -> Proof_global.t)
+  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
+  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
+  | VtReadProof of (pstate:Proof_global.t -> unit)
 
 let interp_functional_vernac c ~pstate =
   let open Proof_global in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 552be6e407..06a08e5e6b 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -44,9 +44,9 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 (** Helper *)
 val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a
 
-val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.pstate -> 'a) -> 'a
+val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> 'a) -> 'a
 
-val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.pstate -> Proof_global.pstate) -> Proof_global.stack option
+val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> Proof_global.t) -> Proof_global.stack option
 
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
@@ -57,11 +57,11 @@ val test_mode : bool ref
 type functional_vernac =
   | VtDefault of (unit -> unit)
   | VtModifyProofStack of (pstate:Proof_global.stack option -> Proof_global.stack option)
-  | VtMaybeOpenProof of (unit -> Proof_global.pstate option)
-  | VtOpenProof of (unit -> Proof_global.pstate)
-  | VtModifyProof of (pstate:Proof_global.pstate -> Proof_global.pstate)
-  | VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
-  | VtReadProof of (pstate:Proof_global.pstate -> unit)
+  | VtMaybeOpenProof of (unit -> Proof_global.t option)
+  | VtOpenProof of (unit -> Proof_global.t)
+  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
+  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
+  | VtReadProof of (pstate:Proof_global.t -> unit)
 
 val interp_functional_vernac
   : functional_vernac
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index f52cd6a829..b0f3c572e5 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -25,7 +25,7 @@ type t = {
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
-val pstate : t -> Proof_global.pstate option
+val pstate : t -> Proof_global.t option
 
 val freeze_interp_state : marshallable:bool -> t
 val unfreeze_interp_state : t -> unit