[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

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