Rename Proof_global.{pstate -> t}

3 files changed, 32 insertions, 32 deletions

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