Rename Proof_global.{pstate -> t}

8 files changed, 32 insertions, 32 deletions

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