diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-27 23:22:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-17 02:19:11 +0200 |
| commit | 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 (patch) | |
| tree | 678afe57f554900aa0c737dc36f53a4c3ece1577 /vernac/vernacentries.mli | |
| parent | d9704f80a4f4b565f77368dbf7c9650d301a233d (diff) | |
[stm] Move interpretation state to Vernacentries
We still don't thread the state there, but this is a start of the
needed infrastructure.
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 |