diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 03:40:45 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 17:38:19 +0100 |
commit | dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch) | |
tree | 228d0aeba91a663b947625fd58cebe5bf4537f08 /vernac/vernacstate.mli | |
parent | d7a5f439de0208c4a543a81158107b8ccecb6ced (diff) |
[plugins] Prepare plugin API for functional handling of state.
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
Diffstat (limited to 'vernac/vernacstate.mli')
-rw-r--r-- | vernac/vernacstate.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli new file mode 100644 index 000000000..63a5b3b1e --- /dev/null +++ b/vernac/vernacstate.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = { (* 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 -> t +val unfreeze_interp_state : t -> unit + +(* WARNING: Do not use, it will go away in future releases *) +val invalidate_cache : unit -> unit |