diff options
| author | Gaëtan Gilbert | 2019-05-20 17:08:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (patch) | |
| tree | 9bf108186e892513ac4a949a3b6ddf31c05ef328 /vernac/vernacentries.mli | |
| parent | 788b47d9dd70dc9f8057d4a9353ed24f091ea917 (diff) | |
Rename Proof_global.{t -> stack}
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 12 |
1 files changed, 6 insertions, 6 deletions
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 |