Rename Proof_global.{t -> stack}

7 files changed, 22 insertions, 22 deletions

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"]