[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.

15 files changed, 159 insertions, 116 deletions

diff --git a/API/API.ml b/API/API.ml
index f588fe193..78d9c0c26 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -275,6 +275,7 @@ module Command = Command
 module Classes = Classes
 (* module Record *)
 (* module Assumptions *)
+module Vernacstate = Vernacstate
 module Vernacinterp = Vernacinterp
 module Mltop = Mltop
 module Topfmt = Topfmt
diff --git a/API/API.mli b/API/API.mli
index 704f1a356..8a4a6cc89 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5929,14 +5929,30 @@ sig
     Names.Id.t
 end
 
+module Vernacstate :
+sig
+
+  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) *)
+  }
+
+  (* XXX: This should not be exported *)
+  val freeze_interp_state : Summary.marshallable -> t
+  val unfreeze_interp_state : t -> unit
+
+end
+
 module Vernacinterp :
 sig
+
   type deprecation = bool
 
-  type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
+  type vernac_command =
+    Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t
 
-  val vinterp_add : deprecation -> Vernacexpr.extend_name ->
-    vernac_command -> unit
+  val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
 
 end
 
@@ -5958,15 +5974,6 @@ 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 freeze_interp_state : Summary.marshallable -> interp_state
-  val unfreeze_interp_state : interp_state -> unit
-
   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
@@ -5998,7 +6005,7 @@ sig
   val get_doc : Feedback.doc_id -> doc
 
   val state_of_id : doc:doc ->
-    Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
+    Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
 end
 
 (************************************************************************)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b4c8ae33c..5b09436c2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -508,7 +508,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun _ -> in_current_context constr_display c)
+           (fun _ st -> in_current_context constr_display c; st)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
@@ -524,7 +524,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun _ -> in_current_context print_pure_constr c)
+           (fun _ st -> in_current_context print_pure_constr c; st)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 874712124..12308bede 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -158,18 +158,26 @@ EXTEND
   deprecation:
     [ [ "DEPRECATED" -> () ] ]
   ;
-  (* spiwack: comment-by-guessing: it seems that the isolated string (which
-      otherwise could have been another argument) is not passed to the
-      VernacExtend interpreter function to discriminate between the clauses. *)
+  (* spiwack: comment-by-guessing: it seems that the isolated string
+      (which otherwise could have been another argument) is not passed
+      to the VernacExtend interpreter function to discriminate between
+      the clauses. *)
+
+  (* ejga: Due to the LocalityFixme abomination we cannot eta-expand
+      [e] as we'd like to, so we need to use the below mess with [fun
+      st -> st].
+
+      At some point We should solve the mess and extend
+      vernacextend.mlp with locality info. *)
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< fun loc -> $e$ >> in
+      let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in
       { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< fun loc -> $e$ >> in
+      let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in
       { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e9102e9c8..61d207b95 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -550,11 +550,11 @@ type tcc_lemma_value =
   | Value of constr
   | Not_needed
 
-(* We only "purify" on exceptions *)
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
 let funind_purify f x =
-  let st = Vernacentries.freeze_interp_state `No in
+  let st = Vernacstate.freeze_interp_state `No in
   try f x
   with e ->
     let e = CErrors.push e in
-    Vernacentries.unfreeze_interp_state st;
+    Vernacstate.unfreeze_interp_state st;
     Exninfo.iraise e
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 01b75e496..77642946c 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -46,7 +46,7 @@ let simple_goal sigma g gs =
 let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
-  | `Valid (Some { Vernacentries.proof }) ->
+  | `Valid (Some { Vernacstate.proof }) ->
        let proof = Proof_global.proof_of_state proof in
        let focused, r1, r2, r3, sigma = Proof.proof proof in
        let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
diff --git a/stm/stm.ml b/stm/stm.ml
index b394c3a13..a3a14a840 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -25,14 +25,14 @@ open Vernacexpr
 
 (* Protect against state changes *)
 let stm_purify f x =
-  let st = Vernacentries.freeze_interp_state `No in
+  let st = Vernacstate.freeze_interp_state `No in
   try
     let res = f x in
-    Vernacentries.unfreeze_interp_state st;
+    Vernacstate.unfreeze_interp_state st;
     res
   with e ->
     let e = CErrors.push e in
-    Vernacentries.unfreeze_interp_state st;
+    Vernacstate.unfreeze_interp_state st;
     Exninfo.iraise e
 
 let execution_error ?loc state_id msg =
@@ -165,7 +165,7 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name;
 type cached_state =
   | Empty
   | Error of Exninfo.iexn
-  | Valid of Vernacentries.interp_state
+  | Valid of Vernacstate.t
 
 type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
 type backup = { mine : branch; others : branch list }
@@ -735,16 +735,16 @@ module State : sig
   val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
 
   (* to send states across worker/master *)
-  val get_cached : Stateid.t -> Vernacentries.interp_state
-  val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool
+  val get_cached : Stateid.t -> Vernacstate.t
+  val same_env : Vernacstate.t -> Vernacstate.t -> bool
 
   type proof_part
 
   type partial_state =
-    [ `Full of Vernacentries.interp_state
+    [ `Full of Vernacstate.t
     | `ProofOnly of Stateid.t * proof_part ]
 
-  val proof_part_of_frozen : Vernacentries.interp_state -> proof_part
+  val proof_part_of_frozen : Vernacstate.t -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
   (* Handlers for initial state, prior to document creation. *)
@@ -757,8 +757,6 @@ module State : sig
 
 end = struct (* {{{ *)
 
-  open Vernacentries
-
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
   let cur_id = ref Stateid.dummy
@@ -768,15 +766,15 @@ end = struct (* {{{ *)
     Proof_global.state * Summary.frozen_bits (* only meta counters *)
 
   type partial_state =
-    [ `Full of Vernacentries.interp_state
+    [ `Full of Vernacstate.t
     | `ProofOnly of Stateid.t * proof_part ]
 
-  let proof_part_of_frozen { Vernacentries.proof; system } =
+  let proof_part_of_frozen { Vernacstate.proof; system } =
     proof,
     Summary.project_summary (States.summary_of_state system) summary_pstate
 
   let freeze marshallable id =
-    VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable))
+    VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable))
 
   let freeze_invalid id iexn = VCS.set_state id (Error iexn)
 
@@ -800,7 +798,7 @@ end = struct (* {{{ *)
   let install_cached id =
     match VCS.get_info id with
     | { state = Valid s } ->
-       Vernacentries.unfreeze_interp_state s;
+       Vernacstate.unfreeze_interp_state s;
        cur_id := id
 
     | { state = Error ie } ->
@@ -819,6 +817,7 @@ end = struct (* {{{ *)
     with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
 
   let assign id what =
+    let open Vernacstate in
     if VCS.get_state id <> Empty then () else
     try match what with
     | `Full s ->
@@ -826,7 +825,7 @@ end = struct (* {{{ *)
            try
             let prev = (VCS.visit id).next in
             if is_cached_and_valid prev
-            then { s with Vernacentries.proof = 
+            then { s with proof =
               Proof_global.copy_terminators
                 ~src:(get_cached prev).proof ~tgt:s.proof }
             else s
@@ -854,7 +853,7 @@ end = struct (* {{{ *)
         execution_error ?loc id (iprint (e, info));
         (e, Stateid.add info ~valid id)
 
-  let same_env { system = s1 } { system = s2 } =
+  let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
     let s1 = States.summary_of_state s1 in
     let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in
     let s2 = States.summary_of_state s2 in
@@ -902,11 +901,11 @@ end = struct (* {{{ *)
   let init_state = ref None
 
   let register_root_state () =
-    init_state := Some (Vernacentries.freeze_interp_state `No)
+    init_state := Some (Vernacstate.freeze_interp_state `No)
 
   let restore_root_state () =
     cur_id := Stateid.dummy;
-    Vernacentries.unfreeze_interp_state (Option.get !init_state);
+    Vernacstate.unfreeze_interp_state (Option.get !init_state);
 
 end (* }}} *)
 
@@ -1001,7 +1000,7 @@ end
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
    reduced... *)
-let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state =
+let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t =
   (* The Stm will gain the capability to interpret commmads affecting
      the whole document state, such as backtrack, etc... so we start
      to design the stm command interpreter now *)
@@ -1437,19 +1436,19 @@ end = struct (* {{{ *)
        * a bad fixpoint *)
       let fix_exn = Future.fix_exn_of future_proof in
       (* STATE: We use the current installed imperative state *)
-      let st = Vernacentries.freeze_interp_state `No in
+      let st = Vernacstate.freeze_interp_state `No in
       if not drop then begin
         let checked_proof = Future.chain future_proof (fun p ->
 
           (* Unfortunately close_future_proof and friends are not pure so we need
              to set the state manually here *)
-          Vernacentries.unfreeze_interp_state st;
+          Vernacstate.unfreeze_interp_state st;
           let pobject, _ =
             Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
 
-          let st = Vernacentries.freeze_interp_state `No in
+          let st = Vernacstate.freeze_interp_state `No in
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
@@ -1457,7 +1456,7 @@ end = struct (* {{{ *)
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
-      Vernacentries.unfreeze_interp_state st;
+      Vernacstate.unfreeze_interp_state st;
       RespBuiltProof(proof,time)
     with
     | e when CErrors.noncritical e || e = Stack_overflow ->
@@ -1598,7 +1597,7 @@ end = struct (* {{{ *)
        * => takes nothing from the itermediate states.
        *)
       (* STATE We use the state resulting from reaching start. *)
-      let st = Vernacentries.freeze_interp_state `No in
+      let st = Vernacstate.freeze_interp_state `No in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
           expr = (VernacEndProof (Proved (Opaque,None))) });
@@ -1855,7 +1854,7 @@ end = struct (* {{{ *)
          * => captures state id in a future closure, which will
            discard execution state but for the proof + univs.
         *)
-        let st = Vernacentries.freeze_interp_state `No in
+        let st = Vernacstate.freeze_interp_state `No in
         ignore(stm_vernac_interp r_state_fb st ast);
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
@@ -1895,7 +1894,7 @@ end = struct (* {{{ *)
         | VernacRedirect (_,(_,e)) -> find ~time ~fail e
         | VernacFail e -> find ~time ~fail:true e
         | e -> e, time, fail in find ~time:false ~fail:false e in
-    let st = Vernacentries.freeze_interp_state `No in
+    let st = Vernacstate.freeze_interp_state `No in
     Vernacentries.with_fail st fail (fun () ->
     (if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -1989,7 +1988,7 @@ end = struct (* {{{ *)
     VCS.print ();
     Reach.known_state ~cache:`No r_where;
     (* STATE *)
-    let st = Vernacentries.freeze_interp_state `No in
+    let st = Vernacstate.freeze_interp_state `No in
     try
       (* STATE SPEC:
        * - start: r_where
@@ -2203,7 +2202,7 @@ let known_state ?(redefine_qed=false) ~cache id =
              Proofview.give_up else Proofview.tclUNIT ()
               end in
            match (VCS.get_info base_state).state with
-           | Valid { Vernacentries.proof } ->
+           | Valid { Vernacstate.proof } ->
                Proof_global.unfreeze proof;
                Proof_global.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
@@ -2213,7 +2212,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 * - end  : maybe after recovery command.
                *)
                (* STATE: We use an updated state with proof *)
-               let st = Vernacentries.freeze_interp_state `No in
+               let st = Vernacstate.freeze_interp_state `No in
                Option.iter (fun expr -> ignore(stm_vernac_interp id st {
                   verbose = true; loc = None; expr; indentation = 0;
                   strlen = 0 } ))
@@ -2293,7 +2292,7 @@ let known_state ?(redefine_qed=false) ~cache id =
             resilient_tactic id cblock (fun () ->
               reach view.next;
               (* State resulting from reach *)
-              let st = Vernacentries.freeze_interp_state `No in
+              let st = Vernacstate.freeze_interp_state `No in
               ignore(stm_vernac_interp id st x)
             );
 	    if eff then update_global_env ()
@@ -2303,13 +2302,13 @@ let known_state ?(redefine_qed=false) ~cache id =
            | Flags.APon | Flags.APonLazy ->
              resilient_command reach view.next
            | Flags.APoff -> reach view.next);
-          let st = Vernacentries.freeze_interp_state `No in
+          let st = Vernacstate.freeze_interp_state `No in
           ignore(stm_vernac_interp id st x);
           if eff then update_global_env ()
         ), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             resilient_command reach view.next;
-            let st = Vernacentries.freeze_interp_state `No in
+            let st = Vernacstate.freeze_interp_state `No in
             ignore(stm_vernac_interp id st x);
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
@@ -2318,7 +2317,7 @@ let known_state ?(redefine_qed=false) ~cache id =
             reach view.next;
 
             (try
-               let st = Vernacentries.freeze_interp_state `No in
+               let st = Vernacstate.freeze_interp_state `No in
                ignore(stm_vernac_interp id st x);
             with e when CErrors.noncritical e ->
               let (e, info) = CErrors.push e in
@@ -2369,7 +2368,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                       Proof_global.close_future_proof ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
-                    let st = Vernacentries.freeze_interp_state `No in
+                    let st = Vernacstate.freeze_interp_state `No in
                     ignore(stm_vernac_interp id ~proof st x);
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
@@ -2378,7 +2377,7 @@ let known_state ?(redefine_qed=false) ~cache id =
               ), (if redefine_qed then `No else `Yes), true
           | `Sync (name, `Immediate) -> (fun () -> 
                 reach eop;
-                let st = Vernacentries.freeze_interp_state `No in
+                let st = Vernacstate.freeze_interp_state `No in
                 ignore(stm_vernac_interp id st x);
                 Proof_global.discard_all ()
               ), `Yes, true
@@ -2401,7 +2400,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 if keep != VtKeepAsAxiom then
                   reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
-                let st = Vernacentries.freeze_interp_state `No in
+                let st = Vernacstate.freeze_interp_state `No in
                 ignore(stm_vernac_interp id ?proof st x);
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
@@ -2419,7 +2418,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           aux (collect_proof keep (view.next, x) brname brinfo eop)
       | `Sideff (ReplayCommand x,_) -> (fun () ->
             reach view.next;
-            let st = Vernacentries.freeze_interp_state `No in
+            let st = Vernacstate.freeze_interp_state `No in
             ignore(stm_vernac_interp id st x);
             update_global_env ()
           ), cache, true
@@ -2688,7 +2687,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
       | VtQuery (false,route), VtNow ->
         let query_sid = VCS.cur_tip () in
         (try
-           let st = Vernacentries.freeze_interp_state `No in
+           let st = Vernacstate.freeze_interp_state `No in
            ignore(stm_vernac_interp ~route query_sid st x)
          with e ->
            let e = CErrors.push e in
@@ -2762,7 +2761,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
 
       (* Side effect on all branches *)
       | VtUnknown, _ when expr = VernacToplevelControl Drop ->
-        let st = Vernacentries.freeze_interp_state `No in
+        let st = Vernacstate.freeze_interp_state `No in
         ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
         `Ok
 
@@ -2790,7 +2789,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
             VCS.checkout VCS.Branch.master;
             let mid = VCS.get_branch_pos VCS.Branch.master in
             let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in
-            let st = Vernacentries.freeze_interp_state `No in
+            let st = Vernacstate.freeze_interp_state `No in
             ignore(stm_vernac_interp id st x);
             (* Vernac x may or may not start a proof *)
             if not in_proof && Proof_global.there_are_pending_proofs () then
diff --git a/stm/stm.mli b/stm/stm.mli
index 31f4599d3..9fd35a0d3 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -220,7 +220,7 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
 val get_doc : Feedback.doc_id -> doc
 
 val state_of_id : doc:doc ->
-  Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
+  Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
 
 (* Queries for backward compatibility *)
 val current_proof_depth : doc:doc -> int
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 850902d6b..8673155e2 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -15,6 +15,7 @@ Command
 Classes
 Record
 Assumptions
+Vernacstate
 Vernacinterp
 Mltop
 Topfmt
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5bcb3b1e1..a71794f5e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1909,7 +1909,7 @@ let vernac_load interp fname =
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-let interp ?proof ?loc locality poly c =
+let interp ?proof ?loc locality poly st c =
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
@@ -2069,7 +2069,10 @@ let interp ?proof ?loc locality poly c =
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)
-  | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args)
+  | VernacExtend (opn,args) ->
+    (* XXX: Here we are returning the state! :) *)
+    let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in
+    ()
 
 (* Vernaculars that take a locality flag *)
 let check_vernac_supports_locality c l =
@@ -2147,28 +2150,6 @@ let locate_if_not_already ?loc (e, info) =
 exception HasNotFailed
 exception HasFailed of Pp.t
 
-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) *)
-}
-
-let s_cache = ref (States.freeze ~marshallable:`No)
-let s_proof = ref (Proof_global.freeze ~marshallable:`No)
-
-let invalidate_cache () =
-  s_cache := Obj.magic 0;
-  s_proof := Obj.magic 0
-
-let freeze_interp_state marshallable =
-  { system = (s_cache := States.freeze ~marshallable; !s_cache);
-    proof  = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
-    shallow = marshallable = `Shallow }
-
-let unfreeze_interp_state { system; proof } =
-  if (!s_cache != system) then (s_cache := system; States.unfreeze system);
-  if (!s_proof != proof)  then (s_proof := proof;  Proof_global.unfreeze proof)
-
 (* XXX STATE: this type hints that restoring the state should be the
    caller's responsibility *)
 let with_fail st b f =
@@ -2187,8 +2168,8 @@ let with_fail st b f =
                             (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
     with e when CErrors.noncritical e ->
       (* Restore the previous state XXX Careful here with the cache! *)
-      invalidate_cache ();
-      unfreeze_interp_state st;
+      Vernacstate.invalidate_cache ();
+      Vernacstate.unfreeze_interp_state st;
       let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
@@ -2230,8 +2211,8 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
         try
           vernac_timeout begin fun () ->
           if verbosely
-            then Flags.verbosely (interp ?proof ?loc locality poly) c
-            else Flags.silently  (interp ?proof ?loc locality poly) c;
+            then Flags.verbosely (interp ?proof ?loc locality poly st) c
+            else Flags.silently  (interp ?proof ?loc locality poly st) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode;
 	  ignore (Flags.use_polymorphic_flag ())
@@ -2252,7 +2233,9 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
 
+(* XXX: There is a bug here in case of an exception, see @gares
+   comments on the PR *)
 let interp ?verbosely ?proof st cmd =
-  unfreeze_interp_state st;
+  Vernacstate.unfreeze_interp_state st;
   interp ?verbosely ?proof st cmd;
-  freeze_interp_state `No
+  Vernacstate.freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 56635c801..67001bc24 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -14,21 +14,11 @@ 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
-
 (** The main interpretation function of vernacular expressions *)
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-  interp_state ->
-    Vernacexpr.vernac_expr Loc.located -> interp_state
+  Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -40,7 +30,7 @@ val make_cases : string -> string list list
 
 (* XXX STATE: this type hints that restoring the state should be the
    caller's responsibility *)
-val with_fail : interp_state -> bool -> (unit -> unit) -> unit
+val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index d2687161a..1d024386e 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -11,7 +11,8 @@ open Pp
 open CErrors
 
 type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
+type vernac_command = Genarg.raw_generic_argument list -> Loc.t option ->
+  Vernacstate.t -> Vernacstate.t
 
 (* Table of vernac entries *)
 let vernac_tab =
@@ -66,8 +67,9 @@ let call ?locality ?loc (opn,converted_args) =
     let hunk = callback converted_args in
     phase := "Executing command";
     Locality.LocalityFixme.set locality;
-    hunk loc;
-    Locality.LocalityFixme.assert_consumed()
+    let res = hunk loc in
+    Locality.LocalityFixme.assert_consumed ();
+    res
   with
     | Drop -> raise Drop
     | reraise ->
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 84370fdc2..1c66b1c04 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -9,12 +9,16 @@
 (** Interpretation of extended vernac phrases. *)
 
 type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
 
-val vinterp_add : deprecation -> Vernacexpr.extend_name ->
-  vernac_command -> unit
-val overwriting_vinterp_add :
-  Vernacexpr.extend_name -> vernac_command -> unit
+type vernac_command = Genarg.raw_generic_argument list -> Loc.t option ->
+  Vernacstate.t -> Vernacstate.t
+
+val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
+
+val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit
 
 val vinterp_init : unit -> unit
-val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit
+
+val call : ?locality:bool -> ?loc:Loc.t ->
+  Vernacexpr.extend_name * Genarg.raw_generic_argument list ->
+  Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
new file mode 100644
index 000000000..9802a03ca
--- /dev/null
+++ b/vernac/vernacstate.ml
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  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) *)
+}
+
+let s_cache = ref (States.freeze ~marshallable:`No)
+let s_proof = ref (Proof_global.freeze ~marshallable:`No)
+
+let invalidate_cache () =
+  s_cache := Obj.magic 0;
+  s_proof := Obj.magic 0
+
+let freeze_interp_state marshallable =
+  { system = (s_cache := States.freeze ~marshallable; !s_cache);
+    proof  = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
+    shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+  if (!s_cache != system) then (s_cache := system; States.unfreeze system);
+  if (!s_proof != proof)  then (s_proof := proof;  Proof_global.unfreeze proof)
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