diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index aa5621770..c1e1c2eda 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -90,12 +90,15 @@ type pstate = { terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; - proof : Proof.proof; + proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: Univdecls.universe_decl; } +type t = pstate list +type state = t + let make_terminator f = f let apply_terminator f = f @@ -467,8 +470,6 @@ module V82 = struct pid, (goals, strength) end -type state = pstate list - let freeze ~marshallable = match marshallable with | `Yes -> |