Rename Proof_global.{pstate -> t}

8 files changed, 9 insertions, 9 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