From 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 27 May 2017 23:22:04 +0200 Subject: [stm] Move interpretation state to Vernacentries We still don't thread the state there, but this is a start of the needed infrastructure. --- vernac/vernacentries.mli | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'vernac/vernacentries.mli') 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 -- cgit v1.2.3