50 files changed, 105 insertions, 82 deletions

diff --git a/.merlin b/.merlin
index 7410e601b7..bda18d5490 100644
--- a/.merlin
+++ b/.merlin
@@ -34,6 +34,8 @@ S stm
 B stm
 S toplevel
 B toplevel
+S vernac
+B vernac
 
 S tools
 B tools
diff --git a/Makefile.common b/Makefile.common
index 49fe1fd939..2c55d76cc8 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -55,7 +55,7 @@ MKDIR:=install -d
 CORESRCDIRS:=\
   config 	lib		kernel		kernel/byterun	library \
   proofs 	tactics 	pretyping	interp		stm \
-  toplevel	parsing 	printing	intf	engine	ltac
+  toplevel	parsing 	printing	intf	engine	ltac vernac
 
 PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
@@ -83,7 +83,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
-        parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
+        parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
 	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a2ee622215..120cde5e55 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -317,7 +317,10 @@ let constrain_variables init uctx =
   let cstrs = UState.constrain_variables levels uctx in
   Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
 
-let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now
+                (fpl : closed_proof_output Future.computation) =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
@@ -395,8 +398,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
     universes = (universes, binders) },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
-
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
diff --git a/stm/stm.ml b/stm/stm.ml
index 6f34c8dbc3..be3e841cb9 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -24,11 +24,13 @@ open Ppvernac
 open Vernac_classifier
 open Feedback
 
+let execution_error state_id loc msg =
+    feedback ~id:(State state_id)
+      (Message (Error, Some loc, pp_to_richpp msg))
+
 module Hooks = struct
 
 let process_error, process_error_hook = Hook.make ()
-let interp, interp_hook = Hook.make ()
-let with_fail, with_fail_hook = Hook.make ()
 
 let state_computed, state_computed_hook = Hook.make
  ~default:(fun state_id ~in_cache ->
@@ -48,10 +50,6 @@ let parse_error, parse_error_hook = Hook.make
  ~default:(fun id loc msg ->
         feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
 
-let execution_error, execution_error_hook = Hook.make
- ~default:(fun state_id loc msg ->
-    feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) ()
-
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
 
@@ -106,24 +104,36 @@ let may_pierce_opaque = function
   | _ -> false
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
-let vernac_interp ?proof id ?route { verbose; loc; expr } =
-  let rec internal_command = function
-    | VernacResetName _ | VernacResetInitial | VernacBack _
-    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
-    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
-    | _ -> false in
-  if internal_command expr then begin
+(* It is currently called 19 times, this number should be certainly
+   reduced... *)
+let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
+  (* 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 *)
+  set_id_for_feedback ?route (State id);
+  Aux_file.record_in_aux_set_at loc;
+  (* We need to check if a command should be filtered from
+   * vernac_entries, as it cannot handle it. This should go away in
+   * future refactorings.
+   *)
+  let rec is_filtered_command = function
+  | VernacResetName _ | VernacResetInitial | VernacBack _
+  | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+  | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+  | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
+  | _ -> false
+  in
+  let aux_interp cmd =
+  if is_filtered_command cmd then
     prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
-  end else begin
-    set_id_for_feedback ?route (State id);
-    Aux_file.record_in_aux_set_at loc;
+  else match cmd with
+  | expr ->
     prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
-    try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
+    try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
     with e ->
       let e = CErrors.push e in
       iraise Hooks.(call_process_error_once e)
-  end
+  in aux_interp expr
 
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
 let indentation_of_string s =
@@ -860,7 +870,7 @@ end = struct (* {{{ *)
     | None ->
         let loc = Option.default Loc.ghost (Loc.get_loc info) in
         let (e, info) = Hooks.(call_process_error_once (e, info)) in
-        Hooks.(call execution_error id loc (iprint (e, info)));
+        execution_error id loc (iprint (e, info));
         (e, Stateid.add info ~valid id)
 
   let same_env { system = s1 } { system = s2 } =
@@ -910,7 +920,6 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
-
 (****************************** CRUFT *****************************************)
 (******************************************************************************)
 
@@ -1287,7 +1296,7 @@ end = struct (* {{{ *)
         let info = Stateid.add ~valid:start Exninfo.null start in
         let e = (RemoteException (strbrk s), info) in
         t_assign (`Exn e);
-        Hooks.(call execution_error start Loc.ghost (strbrk s));
+        execution_error start Loc.ghost (strbrk s);
         feedback (InProgress ~-1)
 
   let build_proof_here ~drop_pt (id,valid) loc eop =
@@ -1750,7 +1759,7 @@ end = struct (* {{{ *)
         | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
         | VernacFail e -> find time true e
         | _ -> e, time, fail in find false false e in
-    Hooks.call Hooks.with_fail fail (fun () ->
+    Vernacentries.with_fail fail (fun () ->
     (if time then System.with_time false else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
@@ -2946,12 +2955,8 @@ let show_script ?proof () =
 let state_computed_hook = Hooks.state_computed_hook
 let state_ready_hook = Hooks.state_ready_hook
 let parse_error_hook = Hooks.parse_error_hook
-let execution_error_hook = Hooks.execution_error_hook
 let forward_feedback_hook = Hooks.forward_feedback_hook
 let process_error_hook = Hooks.process_error_hook
-let interp_hook = Hooks.interp_hook
-let with_fail_hook = Hooks.with_fail_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
-let get_fix_exn () = !State.fix_exn_ref
 let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index b8a2a38596..36341a5d51 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -184,7 +184,6 @@ val register_proof_block_delimiter :
 val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
 val parse_error_hook :
   (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
@@ -218,7 +217,3 @@ val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
 
 (* Hooks to be set by other Coq components in order to break file cycles *)
 val process_error_hook : Future.fix_exn Hook.t
-val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
-  Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
-val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
-val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 939ee187ae..4b254e8113 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -4,7 +4,6 @@ Vcs
 TQueue
 WorkerPool
 Vernac_classifier
-Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
 Stm
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7dd5f2a14..624b9ced7d 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -51,7 +51,7 @@ let lib_dirs =
   ["kernel"; "lib"; "library"; "parsing";
    "pretyping"; "interp"; "printing"; "intf";
    "proofs"; "tactics"; "tools"; "ltacprof";
-   "toplevel"; "stm"; "grammar"; "config";
+   "vernac"; "stm"; "toplevel"; "grammar"; "config";
    "ltac"; "engine"]
 
 
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index eaf938e8ce..645b3665e0 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -75,6 +75,7 @@ let std_includes basedir =
   let rebase d = match basedir with None -> d | Some base -> base / d in
   ["-I"; rebase ".";
    "-I"; rebase "lib";
+   "-I"; rebase "vernac";       (* For Mltop *)
    "-I"; rebase "toplevel";
    "-I"; rebase "kernel/byterun";
    "-I"; Envars.camlp4lib () ] @
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index d689223639..10bf486476 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,19 +1,3 @@
-Himsg
-ExplainErr
-Class
-Locality
-Metasyntax
-Auto_ind_decl
-Search
-Indschemes
-Obligations
-Command
-Classes
-Record
-Assumptions
-Vernacinterp
-Mltop
-Vernacentries
 Vernac
 Usage
 Coqloop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c1a659c38d..f914f83b9b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -343,7 +343,7 @@ let compile verbosely f =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile v f = 
+let compile v f =
   ignore(CoqworkmgrApi.get 1);
   compile v f;
   CoqworkmgrApi.giveback 1
diff --git a/toplevel/assumptions.ml b/vernac/assumptions.ml
index 8865cd6469..8865cd6469 100644
--- a/toplevel/assumptions.ml
+++ b/vernac/assumptions.ml
diff --git a/toplevel/assumptions.mli b/vernac/assumptions.mli
index 0726757839..0726757839 100644
--- a/toplevel/assumptions.mli
+++ b/vernac/assumptions.mli
diff --git a/toplevel/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e9449..594f2e9449 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
diff --git a/toplevel/auto_ind_decl.mli b/vernac/auto_ind_decl.mli
index 60232ba8f4..60232ba8f4 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
diff --git a/toplevel/class.ml b/vernac/class.ml
index 0dc7990143..0dc7990143 100644
--- a/toplevel/class.ml
+++ b/vernac/class.ml
diff --git a/toplevel/class.mli b/vernac/class.mli
index 5f9ae28f62..5f9ae28f62 100644
--- a/toplevel/class.mli
+++ b/vernac/class.mli
diff --git a/toplevel/classes.ml b/vernac/classes.ml
index 6512f3defa..6512f3defa 100644
--- a/toplevel/classes.ml
+++ b/vernac/classes.ml
diff --git a/toplevel/classes.mli b/vernac/classes.mli
index d2cb788eae..d2cb788eae 100644
--- a/toplevel/classes.mli
+++ b/vernac/classes.mli
diff --git a/toplevel/command.ml b/vernac/command.ml
index 049f58aa26..049f58aa26 100644
--- a/toplevel/command.ml
+++ b/vernac/command.ml
diff --git a/toplevel/command.mli b/vernac/command.mli
index 616afb91f0..616afb91f0 100644
--- a/toplevel/command.mli
+++ b/vernac/command.mli
diff --git a/toplevel/discharge.ml b/vernac/discharge.ml
index e24d5e74fb..e24d5e74fb 100644
--- a/toplevel/discharge.ml
+++ b/vernac/discharge.ml
diff --git a/toplevel/discharge.mli b/vernac/discharge.mli
index 18d1b67766..18d1b67766 100644
--- a/toplevel/discharge.mli
+++ b/vernac/discharge.mli
diff --git a/toplevel/doc.tex b/vernac/doc.tex
index f2550fda11..f2550fda11 100644
--- a/toplevel/doc.tex
+++ b/vernac/doc.tex
diff --git a/toplevel/explainErr.ml b/vernac/explainErr.ml
index 17897460c0..17897460c0 100644
--- a/toplevel/explainErr.ml
+++ b/vernac/explainErr.ml
diff --git a/toplevel/explainErr.mli b/vernac/explainErr.mli
index a67c887af3..a67c887af3 100644
--- a/toplevel/explainErr.mli
+++ b/vernac/explainErr.mli
diff --git a/toplevel/himsg.ml b/vernac/himsg.ml
index 6cff805fc2..6cff805fc2 100644
--- a/toplevel/himsg.ml
+++ b/vernac/himsg.ml
diff --git a/toplevel/himsg.mli b/vernac/himsg.mli
index ced54fd279..ced54fd279 100644
--- a/toplevel/himsg.mli
+++ b/vernac/himsg.mli
diff --git a/toplevel/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194c..85d0b6194c 100644
--- a/toplevel/ind_tables.ml
+++ b/vernac/ind_tables.ml
diff --git a/toplevel/ind_tables.mli b/vernac/ind_tables.mli
index 20f30d6d16..20f30d6d16 100644
--- a/toplevel/ind_tables.mli
+++ b/vernac/ind_tables.mli
diff --git a/toplevel/indschemes.ml b/vernac/indschemes.ml
index f7e3f0d954..f7e3f0d954 100644
--- a/toplevel/indschemes.ml
+++ b/vernac/indschemes.ml
diff --git a/toplevel/indschemes.mli b/vernac/indschemes.mli
index e5d79fd514..e5d79fd514 100644
--- a/toplevel/indschemes.mli
+++ b/vernac/indschemes.mli
diff --git a/stm/lemmas.ml b/vernac/lemmas.ml
index 55f33be399..55f33be399 100644
--- a/stm/lemmas.ml
+++ b/vernac/lemmas.ml
diff --git a/stm/lemmas.mli b/vernac/lemmas.mli
index 39c089be9f..39c089be9f 100644
--- a/stm/lemmas.mli
+++ b/vernac/lemmas.mli
diff --git a/toplevel/locality.ml b/vernac/locality.ml
index 03640676e6..03640676e6 100644
--- a/toplevel/locality.ml
+++ b/vernac/locality.ml
diff --git a/toplevel/locality.mli b/vernac/locality.mli
index 2ec392eefc..2ec392eefc 100644
--- a/toplevel/locality.mli
+++ b/vernac/locality.mli
diff --git a/toplevel/metasyntax.ml b/vernac/metasyntax.ml
index 0aaf6afd7e..0aaf6afd7e 100644
--- a/toplevel/metasyntax.ml
+++ b/vernac/metasyntax.ml
diff --git a/toplevel/metasyntax.mli b/vernac/metasyntax.mli
index 57c1204022..57c1204022 100644
--- a/toplevel/metasyntax.mli
+++ b/vernac/metasyntax.mli
diff --git a/toplevel/mltop.ml b/vernac/mltop.ml
index 2396cf04a4..2396cf04a4 100644
--- a/toplevel/mltop.ml
+++ b/vernac/mltop.ml
diff --git a/toplevel/mltop.mli b/vernac/mltop.mli
index 6633cb9372..6633cb9372 100644
--- a/toplevel/mltop.mli
+++ b/vernac/mltop.mli
diff --git a/toplevel/obligations.ml b/vernac/obligations.ml
index 9ada043171..c1d9ae48a5 100644
--- a/toplevel/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,6 +20,12 @@ open Pp
 open CErrors
 open Util
 
+(* EJGA: This should go away, no more need for fix_exn  *)
+module Stm = struct
+    let u = (fun x -> x)
+    let get_fix_exn () = u
+end
+
 module NamedDecl = Context.Named.Declaration
 
 let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
diff --git a/toplevel/obligations.mli b/vernac/obligations.mli
index 80b6891447..80b6891447 100644
--- a/toplevel/obligations.mli
+++ b/vernac/obligations.mli
diff --git a/toplevel/record.ml b/vernac/record.ml
index d5faafaf89..d5faafaf89 100644
--- a/toplevel/record.ml
+++ b/vernac/record.ml
diff --git a/toplevel/record.mli b/vernac/record.mli
index c50e577860..c50e577860 100644
--- a/toplevel/record.mli
+++ b/vernac/record.mli
diff --git a/toplevel/search.ml b/vernac/search.ml
index e1b56b1319..e1b56b1319 100644
--- a/toplevel/search.ml
+++ b/vernac/search.ml
diff --git a/toplevel/search.mli b/vernac/search.mli
index c9167c485d..c9167c485d 100644
--- a/toplevel/search.mli
+++ b/vernac/search.mli
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
new file mode 100644
index 0000000000..94ef54f70f
--- /dev/null
+++ b/vernac/vernac.mllib
@@ -0,0 +1,17 @@
+Lemmas
+Himsg
+ExplainErr
+Class
+Locality
+Metasyntax
+Auto_ind_decl
+Search
+Indschemes
+Obligations
+Command
+Classes
+Record
+Assumptions
+Vernacinterp
+Mltop
+Vernacentries
diff --git a/toplevel/vernacentries.ml b/vernac/vernacentries.ml
index 862a761b23..15f89e4b86 100644
--- a/toplevel/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -517,8 +517,10 @@ let qed_display_script = ref true
 let vernac_end_proof ?proof = function
   | Admitted -> save_proof ?proof Admitted
   | Proved (_,_) as e ->
+    (*
     if is_verbose () && !qed_display_script && !Flags.coqtop_ui then
       Stm.show_script ?proof ();
+    *)
     save_proof ?proof e
 
   (* A stupid macro that should be replaced by ``Exact c. Save.'' all along
@@ -1882,7 +1884,7 @@ let vernac_show = let open Feedback in function
       Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n)
   | ShowProof -> show_proof ()
   | ShowNode -> show_node ()
-  | ShowScript -> Stm.show_script ()
+  | ShowScript -> (* Stm.show_script () *) ()
   | ShowExistentials -> show_top_evars ()
   | ShowUniverses -> show_universes ()
   | ShowTree -> show_prooftree ()
@@ -1909,6 +1911,12 @@ let vernac_check_guard () =
 
 exception End_of_input
 
+(* XXX: This won't properly set the proof mode, as of today, it is
+   controlled by the STM. Thus, we would need access information from
+   the classifier. The proper fix is to move it to the STM, however,
+   the way the proof mode is set there makes the task non trivial
+   without a considerable amount of refactoring.
+ *)
 let vernac_load interp fname =
   let interp x =
     let proof_mode = Proof_global.get_default_proof_mode_name () in
@@ -1936,16 +1944,45 @@ let vernac_load interp fname =
 let interp ?proof ~loc locality poly c =
   prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
-  (* Done later in this file *)
+  (* The below vernac are candidates for removal from the main type
+     and to be put into a new doc_command datatype: *)
+
   | VernacLoad _ -> assert false
+
+  (* Done later in this file *)
   | VernacFail _ -> assert false
   | VernacTime _ -> assert false
   | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
   | VernacStm _ -> assert false
 
+  (* The STM should handle that, but LOAD bypasses the STM... *)
+  | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
+  | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
+  | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
+  | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
+  | VernacBacktrack _ -> CErrors.user_err  (str "Backtrack cannot be used through the Load command")
+
+  (* Toplevel control *)
+  | VernacToplevelControl e -> raise e
+
+  (* Resetting *)
+  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm")
+  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm")
+  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm")
+  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm")
+
+  (* Horrible Hack that should die. *)
   | VernacError e -> raise e
 
+  (* This one is possible to handle here *)
+  | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
+
+  (* Handled elsewhere *)
+  | VernacProgram _
+  | VernacPolymorphic _
+  | VernacLocal _ -> assert false
+
   (* Syntax *)
   | VernacSyntaxExtension (local,sl) ->
       vernac_syntax_extension locality local sl
@@ -2017,12 +2054,6 @@ let interp ?proof ~loc locality poly c =
   | VernacWriteState s -> vernac_write_state s
   | VernacRestoreState s -> vernac_restore_state s
 
-  (* Resetting *)
-  | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm")
-  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm")
-  | VernacBack _ -> anomaly (str "VernacBack not handled by Stm")
-  | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
-
   (* Commands *)
   | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
   | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
@@ -2054,14 +2085,6 @@ let interp ?proof ~loc locality poly c =
   | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
-  (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> CErrors.user_err  (str "Abort cannot be used through the Load command")
-  | VernacAbortAll -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
-  | VernacRestart -> CErrors.user_err  (str "Restart cannot be used through the Load command")
-  | VernacUndo _ -> CErrors.user_err  (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _ -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
-  | VernacBacktrack _ -> CErrors.user_err  (str "Backtrack cannot be used through the Load command")
-  
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
   | VernacFocus n -> vernac_focus n
@@ -2084,17 +2107,10 @@ let interp ?proof ~loc locality poly c =
       Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes";
       vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
-  (* Toplevel control *)
-  | VernacToplevelControl e -> raise e
 
   (* Extensions *)
   | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)
 
-  (* Handled elsewhere *)
-  | VernacProgram _
-  | VernacPolymorphic _
-  | VernacLocal _ -> assert false
-
 (* Vernaculars that take a locality flag *)
 let check_vernac_supports_locality c l =
   match l, c with
@@ -2253,6 +2269,3 @@ let interp ?(verbosely=true) ?proof (loc,c) =
   in
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
-
-let () = Hook.set Stm.interp_hook interp
-let () = Hook.set Stm.with_fail_hook with_fail
diff --git a/toplevel/vernacentries.mli b/vernac/vernacentries.mli
index 7cdc8dd064..7cdc8dd064 100644
--- a/toplevel/vernacentries.mli
+++ b/vernac/vernacentries.mli
diff --git a/toplevel/vernacinterp.ml b/vernac/vernacinterp.ml
index f26ef460dd..f26ef460dd 100644
--- a/toplevel/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
diff --git a/toplevel/vernacinterp.mli b/vernac/vernacinterp.mli
index 5149b5416d..5149b5416d 100644
--- a/toplevel/vernacinterp.mli
+++ b/vernac/vernacinterp.mli