Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.

15 files changed, 160 insertions, 117 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 6c696ebb8..864fff9e0 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
@@ -2204,7 +2203,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;
@@ -2214,7 +2213,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 } ))
@@ -2294,7 +2293,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 ()
@@ -2304,13 +2303,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
@@ -2319,7 +2318,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
@@ -2370,7 +2369,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
@@ -2379,7 +2378,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
@@ -2402,7 +2401,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"
@@ -2420,7 +2419,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
@@ -2689,7 +2688,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
@@ -2763,7 +2762,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
 
@@ -2791,7 +2790,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 41fee6bd0..1d024386e 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -11,11 +11,12 @@ 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 =
-  (Hashtbl.create 51 :
+  (Hashtbl.create 211 :
     (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t)
 
 let vinterp_add depr s f =
@@ -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