diff options
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a09011d24..5559e6b81 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,11 +14,22 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +val freeze_interp_state : Summary.marshallable -> interp_state +val unfreeze_interp_state : interp_state -> unit +val _dummy_interp_state : interp_state + (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Vernacexpr.vernac_expr Loc.located -> unit + interp_state -> + Vernacexpr.vernac_expr Loc.located -> interp_state (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |