[stm] Move interpretation state to Vernacentries

We still don't thread the state there, but this is a start of the
needed infrastructure.

1 files changed, 14 insertions, 2 deletions

diff --git a/API/API.mli b/API/API.mli
index 535f6a29b..d4f0872a3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2060,6 +2060,8 @@ end
 
 module States :
 sig
+  type state
+
   val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b
   val with_state_protection : ('a -> 'b) -> 'a -> 'b
 end
@@ -4512,6 +4514,9 @@ end
 
 module Proof_global :
 sig
+
+  type state
+
   type proof_mode = {
       name : string;
       set : unit -> unit ;
@@ -5787,6 +5792,13 @@ end
 
 module Vernacentries :
 sig
+
+  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 dump_global : Libnames.reference Misctypes.or_by_notation -> unit
   val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
                             Evd.evar_map * Redexpr.red_expr) Hook.t
@@ -5814,11 +5826,11 @@ end
 module Stm :
 sig
   type doc
-  type state
 
   val get_doc : Feedback.doc_id -> doc
+
   val state_of_id : doc:doc ->
-    Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+    Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
 end
 
 (************************************************************************)