aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--proofs/proof_global.mli24
-rw-r--r--stm/stm.ml2
-rw-r--r--vernac/lemmas.mli6
-rw-r--r--vernac/vernacentries.ml6
-rw-r--r--vernac/vernacentries.mli12
-rw-r--r--vernac/vernacextend.ml2
-rw-r--r--vernac/vernacextend.mli2
-rw-r--r--vernac/vernacstate.ml2
-rw-r--r--vernac/vernacstate.mli14
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"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:11:19 +0000