Rename Proof_global.{t -> stack}

10 files changed, 37 insertions, 37 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8d7960829b..e26577e8bd 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -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 t = pstate * pstate list
+type stack = pstate * pstate list
 
 let pstate_map f (pf, pfl) = (f pf, List.map f pfl)
 
@@ -77,7 +77,7 @@ let maybe_push ~ontop = function
 
 (*** Proof Global manipulation ***)
 
-let get_all_proof_names (pf : t) =
+let get_all_proof_names (pf : stack) =
   let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in
   pn :: pns
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6984fff63a..aa538bd581 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,16 +13,16 @@
      environment. *)
 
 type pstate
-type t
+type stack
 
-val get_current_pstate : t -> pstate
+val get_current_pstate : stack -> pstate
 
 val get_current_proof_name : pstate -> Names.Id.t
 val get_current_persistence : pstate -> Decl_kinds.goal_kind
-val get_all_proof_names : t -> Names.Id.t list
+val get_all_proof_names : stack -> Names.Id.t list
 
-val discard : Names.lident -> t -> t option
-val discard_current : t -> t option
+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
@@ -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:t option -> pstate -> t
+val push : ontop:stack option -> pstate -> stack
 
-val maybe_push : ontop:t option -> pstate option -> t option
+val maybe_push : ontop:stack option -> pstate 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
@@ -111,15 +111,15 @@ val get_open_goals : pstate -> int
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> stack -> stack * 'a
 val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
+  (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_current_pstate : (pstate -> pstate * 'a) -> t -> t * 'a
-val modify_current_pstate : (pstate -> pstate) -> t -> t
+val with_current_pstate : (pstate -> pstate * 'a) -> stack -> stack * 'a
+val modify_current_pstate : (pstate -> pstate) -> 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
@@ -135,4 +135,4 @@ val get_used_variables : pstate -> Constr.named_context option
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : pstate -> UState.universe_decl
 
-val copy_terminators : src:t -> tgt:t -> t
+val copy_terminators : src:stack -> tgt:stack -> stack
diff --git a/stm/stm.ml b/stm/stm.ml
index 64f9e4aacf..0efea0b8e0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -881,7 +881,7 @@ end = struct (* {{{ *)
   let invalidate_cur_state () = cur_id := Stateid.dummy
 
   type proof_part =
-    Proof_global.t option *
+    Proof_global.stack option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
     Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index ad6eb024aa..e613b79c7b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -61,7 +61,7 @@ val standard_proof_terminator :
   ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
   Proof_global.proof_terminator
 
-val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Id.t
+val fresh_name_for_anonymous_theorem : pstate:Proof_global.stack option -> Id.t
 
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
@@ -77,10 +77,10 @@ val save_proof_admitted
 
 val save_proof_proved
   :  ?proof:Proof_global.closed_proof
-  -> ?ontop:Proof_global.t
+  -> ?ontop:Proof_global.stack
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
-  -> Proof_global.t option
+  -> Proof_global.stack option
 
 val save_pstate_proved
   : pstate:Proof_global.pstate
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 49ce27ee30..8d15191ebe 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1937,7 +1937,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     let sigma, env = get_current_or_global_context ~pstate in
     print_about env sigma ref_or_by_not udecl
 
-let vernac_print ~(pstate : Proof_global.t option) ~atts =
+let vernac_print ~(pstate : Proof_global.stack option) ~atts =
   let pstate = Option.map Proof_global.get_current_pstate pstate in
   let sigma, env = get_current_or_global_context ~pstate in
   function
@@ -2299,7 +2299,7 @@ exception End_of_input
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
+let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
   let pstate = st.Vernacstate.proof in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
@@ -2714,7 +2714,7 @@ let interp ?(verbosely=true) ?proof ~st cmd =
 
 type functional_vernac =
   | VtDefault of (unit -> unit)
-  | VtModifyProofStack of (pstate:Proof_global.t option -> Proof_global.t option)
+  | 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)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 55763d9e51..552be6e407 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,11 +42,11 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
 (** Helper *)
-val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a
+val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a
 
-val with_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate -> 'a) -> 'a
+val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.pstate -> 'a) -> 'a
 
-val modify_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate -> Proof_global.pstate) -> Proof_global.t option
+val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.pstate -> Proof_global.pstate) -> Proof_global.stack option
 
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
@@ -56,7 +56,7 @@ val test_mode : bool ref
 
 type functional_vernac =
   | VtDefault of (unit -> unit)
-  | VtModifyProofStack of (pstate:Proof_global.t option -> Proof_global.t option)
+  | 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)
@@ -65,5 +65,5 @@ type functional_vernac =
 
 val interp_functional_vernac
   : functional_vernac
-  -> pstate:Proof_global.t option
-  -> Proof_global.t option
+  -> pstate:Proof_global.stack option
+  -> Proof_global.stack option
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 008d3d854f..644413cbb9 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -53,7 +53,7 @@ type vernac_when =
   | VtLater
 type vernac_classification = vernac_type * vernac_when
 
-type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.t option -> Proof_global.t option
+type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.stack option -> Proof_global.stack option
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 6189830929..46cee30a1e 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -71,7 +71,7 @@ type vernac_classification = vernac_type * vernac_when
 
 (** Interpretation of extended vernac phrases. *)
 
-type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.t option -> Proof_global.t option
+type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.stack option -> Proof_global.stack option
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 6eb618ad0a..0fbde1ade5 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -30,7 +30,7 @@ end
 type t = {
   parsing : Parser.state;
   system  : States.state;          (* summary + libstack *)
-  proof   : Proof_global.t option; (* proof state *)
+  proof   : Proof_global.stack option; (* proof state *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 3d21b475e9..f52cd6a829 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -21,7 +21,7 @@ end
 type t = {
   parsing : Parser.state;
   system  : States.state;          (* summary + libstack *)
-  proof   : Proof_global.t option; (* proof state *)
+  proof   : Proof_global.stack option; (* proof state *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
@@ -41,11 +41,11 @@ module Proof_global : sig
   open Proof_global
 
   (* Low-level stuff *)
-  val get : unit -> t option
-  val set : t option -> unit
+  val get : unit -> stack option
+  val set : stack option -> unit
 
-  val freeze : marshallable:bool -> t option
-  val unfreeze : t -> unit
+  val freeze : marshallable:bool -> stack option
+  val unfreeze : stack -> unit
 
   exception NoCurrentProof
 
@@ -63,7 +63,7 @@ module Proof_global : sig
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-  val install_state : t -> unit
+  val install_state : stack -> unit
 
   val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
 
@@ -81,7 +81,7 @@ module Proof_global : sig
 
   val get_all_proof_names : unit -> Names.Id.t list
 
-  val copy_terminators : src:t option -> tgt:t option -> t option
+  val copy_terminators : src:stack option -> tgt:stack option -> stack option
 
 end
 [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]