[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 7410e601b..bda18d549 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 49fe1fd93..2c55d76cc 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 a2ee62221..120cde5e5 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 6f34c8dbc..be3e841cb 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 b8a2a3859..36341a5d5 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 939ee187a..4b254e811 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 b7dd5f2a1..624b9ced7 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 eaf938e8c..645b3665e 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 d68922363..10bf48647 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 c1a659c38..f914f83b9 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 8865cd646..8865cd646 100644
--- a/toplevel/assumptions.ml
+++ b/vernac/assumptions.ml
diff --git a/toplevel/assumptions.mli b/vernac/assumptions.mli
index 072675783..072675783 100644
--- a/toplevel/assumptions.mli
+++ b/vernac/assumptions.mli
diff --git a/toplevel/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e944..594f2e944 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 60232ba8f..60232ba8f 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/vernac/auto_ind_decl.mli
diff --git a/toplevel/class.ml b/vernac/class.ml
index 0dc799014..0dc799014 100644
--- a/toplevel/class.ml
+++ b/vernac/class.ml
diff --git a/toplevel/class.mli b/vernac/class.mli
index 5f9ae28f6..5f9ae28f6 100644
--- a/toplevel/class.mli
+++ b/vernac/class.mli
diff --git a/toplevel/classes.ml b/vernac/classes.ml
index 6512f3def..6512f3def 100644
--- a/toplevel/classes.ml
+++ b/vernac/classes.ml
diff --git a/toplevel/classes.mli b/vernac/classes.mli
index d2cb788ea..d2cb788ea 100644
--- a/toplevel/classes.mli
+++ b/vernac/classes.mli
diff --git a/toplevel/command.ml b/vernac/command.ml
index 049f58aa2..049f58aa2 100644
--- a/toplevel/command.ml
+++ b/vernac/command.ml
diff --git a/toplevel/command.mli b/vernac/command.mli
index 616afb91f..616afb91f 100644
--- a/toplevel/command.mli
+++ b/vernac/command.mli
diff --git a/toplevel/discharge.ml b/vernac/discharge.ml
index e24d5e74f..e24d5e74f 100644
--- a/toplevel/discharge.ml
+++ b/vernac/discharge.ml
diff --git a/toplevel/discharge.mli b/vernac/discharge.mli
index 18d1b6776..18d1b6776 100644
--- a/toplevel/discharge.mli
+++ b/vernac/discharge.mli
diff --git a/toplevel/doc.tex b/vernac/doc.tex
index f2550fda1..f2550fda1 100644
--- a/toplevel/doc.tex
+++ b/vernac/doc.tex
diff --git a/toplevel/explainErr.ml b/vernac/explainErr.ml
index 17897460c..17897460c 100644
--- a/toplevel/explainErr.ml
+++ b/vernac/explainErr.ml
diff --git a/toplevel/explainErr.mli b/vernac/explainErr.mli
index a67c887af..a67c887af 100644
--- a/toplevel/explainErr.mli
+++ b/vernac/explainErr.mli
diff --git a/toplevel/himsg.ml b/vernac/himsg.ml
index 6cff805fc..6cff805fc 100644
--- a/toplevel/himsg.ml
+++ b/vernac/himsg.ml
diff --git a/toplevel/himsg.mli b/vernac/himsg.mli
index ced54fd27..ced54fd27 100644
--- a/toplevel/himsg.mli
+++ b/vernac/himsg.mli
diff --git a/toplevel/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194..85d0b6194 100644
--- a/toplevel/ind_tables.ml
+++ b/vernac/ind_tables.ml
diff --git a/toplevel/ind_tables.mli b/vernac/ind_tables.mli
index 20f30d6d1..20f30d6d1 100644
--- a/toplevel/ind_tables.mli
+++ b/vernac/ind_tables.mli
diff --git a/toplevel/indschemes.ml b/vernac/indschemes.ml
index f7e3f0d95..f7e3f0d95 100644
--- a/toplevel/indschemes.ml
+++ b/vernac/indschemes.ml
diff --git a/toplevel/indschemes.mli b/vernac/indschemes.mli
index e5d79fd51..e5d79fd51 100644
--- a/toplevel/indschemes.mli
+++ b/vernac/indschemes.mli
diff --git a/stm/lemmas.ml b/vernac/lemmas.ml
index 55f33be39..55f33be39 100644
--- a/stm/lemmas.ml
+++ b/vernac/lemmas.ml
diff --git a/stm/lemmas.mli b/vernac/lemmas.mli
index 39c089be9..39c089be9 100644
--- a/stm/lemmas.mli
+++ b/vernac/lemmas.mli
diff --git a/toplevel/locality.ml b/vernac/locality.ml
index 03640676e..03640676e 100644
--- a/toplevel/locality.ml
+++ b/vernac/locality.ml
diff --git a/toplevel/locality.mli b/vernac/locality.mli
index 2ec392eef..2ec392eef 100644
--- a/toplevel/locality.mli
+++ b/vernac/locality.mli
diff --git a/toplevel/metasyntax.ml b/vernac/metasyntax.ml
index 0aaf6afd7..0aaf6afd7 100644
--- a/toplevel/metasyntax.ml
+++ b/vernac/metasyntax.ml
diff --git a/toplevel/metasyntax.mli b/vernac/metasyntax.mli
index 57c120402..57c120402 100644
--- a/toplevel/metasyntax.mli
+++ b/vernac/metasyntax.mli
diff --git a/toplevel/mltop.ml b/vernac/mltop.ml
index 2396cf04a..2396cf04a 100644
--- a/toplevel/mltop.ml
+++ b/vernac/mltop.ml
diff --git a/toplevel/mltop.mli b/vernac/mltop.mli
index 6633cb937..6633cb937 100644
--- a/toplevel/mltop.mli
+++ b/vernac/mltop.mli
diff --git a/toplevel/obligations.ml b/vernac/obligations.ml
index 9ada04317..c1d9ae48a 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 80b689144..80b689144 100644
--- a/toplevel/obligations.mli
+++ b/vernac/obligations.mli
diff --git a/toplevel/record.ml b/vernac/record.ml
index d5faafaf8..d5faafaf8 100644
--- a/toplevel/record.ml
+++ b/vernac/record.ml
diff --git a/toplevel/record.mli b/vernac/record.mli
index c50e57786..c50e57786 100644
--- a/toplevel/record.mli
+++ b/vernac/record.mli
diff --git a/toplevel/search.ml b/vernac/search.ml
index e1b56b131..e1b56b131 100644
--- a/toplevel/search.ml
+++ b/vernac/search.ml
diff --git a/toplevel/search.mli b/vernac/search.mli
index c9167c485..c9167c485 100644
--- a/toplevel/search.mli
+++ b/vernac/search.mli
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
new file mode 100644
index 000000000..94ef54f70
--- /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 862a761b2..15f89e4b8 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 7cdc8dd06..7cdc8dd06 100644
--- a/toplevel/vernacentries.mli
+++ b/vernac/vernacentries.mli
diff --git a/toplevel/vernacinterp.ml b/vernac/vernacinterp.ml
index f26ef460d..f26ef460d 100644
--- a/toplevel/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
diff --git a/toplevel/vernacinterp.mli b/vernac/vernacinterp.mli
index 5149b5416..5149b5416 100644
--- a/toplevel/vernacinterp.mli
+++ b/vernac/vernacinterp.mli