Imported Upstream version 8.9.0upstream/8.9.0upstream

19 files changed, 169 insertions, 260 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index b3e1500a..768d94d3 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of Universes.universe_id list
+    | MoreDataUnivLevel of UnivGen.universe_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in
@@ -120,12 +120,11 @@ module Make(T : Task) () = struct
     let proc, ic, oc =
       let rec set_slave_opt = function
         | [] -> !async_proofs_flags_for_workers @
-                ["-toploop"; !T.name^"top";
-                 "-worker-id"; name;
+                ["-worker-id"; name;
                  "-async-proofs-worker-priority";
-                   CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)]
-        | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vio2vo"
+                   CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+        | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
+        | ("-async-proofs" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -134,7 +133,8 @@ module Make(T : Task) () = struct
       let args =
         Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
       let env = Array.append (T.extra_env ()) (Unix.environment ()) in
-    Worker.spawn ~env Sys.argv.(0) args in
+    let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
+    Worker.spawn ~env worker_name args in
     name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
 
   let manager cpanel (id, proc, ic, oc) =
@@ -171,7 +171,7 @@ module Make(T : Task) () = struct
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
     let more_univs n =
-      CList.init n (fun _ -> Universes.new_univ_id ()) in
+      CList.init n (fun _ -> UnivGen.new_univ_id ()) in
 
     let rec kill_if () =
       if not (Worker.is_alive proc) then ()
@@ -310,7 +310,7 @@ module Make(T : Task) () = struct
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
     (* We ask master to allocate universe identifiers *)
-    Universes.set_remote_new_univ_id (bufferize (fun () ->
+    UnivGen.set_remote_new_univ_id (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
       | MoreDataUnivLevel l -> l));
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 36b5d18a..841cc08c 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -11,6 +11,10 @@
 let debug = false
 
 type priority = Low | High
+
+(* Default priority *)
+let async_proofs_worker_priority = ref Low
+
 let string_of_priority = function Low -> "low" | High -> "high"
 let priority_of_string = function
   | "low" -> Low
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 2983b619..be5b2917 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -14,6 +14,9 @@ type priority = Low | High
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
 
+(* Default priority *)
+val async_proofs_worker_priority : priority ref
+
 (* Connects to a work manager if any. If no worker manager, then
    -async-proofs-j and -async-proofs-tac-j are used *)
 val init : priority -> unit
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 23f97612..b8af2bcd 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,8 +23,8 @@ val crawl :
     static_block_declaration option
 
 val unit_val : Stm.DynBlockData.t
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
 val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
 val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
 
@@ -41,7 +41,7 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term evi.evar_concl) &&
+  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 9784de11..eacd3687 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -38,6 +38,6 @@ val crawl :
 val unit_val : Stm.DynBlockData.t
 
 (* Bullets *)
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
 
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
deleted file mode 100644
index 4b85a05a..00000000
--- a/stm/proofworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
-
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib
deleted file mode 100644
index f9f6c22d..00000000
--- a/stm/proofworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Proofworkertop
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
deleted file mode 100644
index aa00102a..00000000
--- a/stm/queryworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
-
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib
deleted file mode 100644
index c2f73089..00000000
--- a/stm/queryworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Queryworkertop
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 3833c802..a5d6ea96 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -28,13 +28,11 @@ let controller h pr pw =
   prerr_endline "starting controller thread";
   let main () =
     let ic, oc = open_bin_connection h pr pw in
-    let rec loop () =
+    let loop () =
       try
         match CThread.thread_friendly_input_value ic with
         | Hello _ -> prerr_endline "internal protocol error"; exit 1
         | ReqDie -> prerr_endline "death sentence received"; exit 0
-        | ReqStats ->
-            output_value oc (RespStats (Gc.quick_stat ())); flush oc; loop ()
       with
       | e ->
         prerr_endline ("control channel broken: " ^ Printexc.to_string e);
diff --git a/stm/stm.ml b/stm/stm.ml
index e1b90bd2..ada7e3e3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -92,11 +92,11 @@ let execution_error ?loc state_id msg =
 module Hooks = struct
 
 let state_computed, state_computed_hook = Hook.make
- ~default:(fun state_id ~in_cache ->
+ ~default:(fun ~doc:_ state_id ~in_cache ->
     feedback ~id:state_id Processed) ()
 
 let state_ready, state_ready_hook = Hook.make
- ~default:(fun state_id -> ()) ()
+ ~default:(fun ~doc:_ state_id -> ()) ()
 
 let forward_feedback, forward_feedback_hook =
   let m = Mutex.create () in
@@ -106,7 +106,7 @@ let forward_feedback, forward_feedback_hook =
         with e -> Mutex.unlock m; raise e) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
- ~default:(fun _ _ -> ()) ()
+ ~default:(fun ~doc:_ _ _ -> ()) ()
 
 include Hook
 
@@ -578,7 +578,7 @@ end = struct (* {{{ *)
     | None -> raise Vcs_aux.Expired
   let set_state id s =
     (get_info id).state <- s;
-    if async_proofs_is_master !cur_opt then Hooks.(call state_ready id)
+    if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
   let get_state id = (get_info id).state
   let reached id =
     let info = get_info id in
@@ -770,6 +770,7 @@ module State : sig
       Warning: an optimization in installed_cached requires that state
       modifying functions are always executed using this wrapper. *)
   val define :
+    doc:doc ->
     ?safe_id:Stateid.t ->
     ?redefine:bool -> ?cache:Summary.marshallable ->
     ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
@@ -919,7 +920,7 @@ end = struct (* {{{ *)
     let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
     e1 == e2
 
-  let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
+  let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
   =
     feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
@@ -938,7 +939,7 @@ end = struct (* {{{ *)
       stm_prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
-        Hooks.(call state_computed id ~in_cache:false);
+        Hooks.(call state_computed ~doc id ~in_cache:false);
       VCS.reached id;
       if Proof_global.there_are_pending_proofs () then
         VCS.goals id (Proof_global.get_open_goals ())
@@ -954,7 +955,7 @@ end = struct (* {{{ *)
         | Some _, None -> (e, info)
         | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
       if cache = `Yes || cache = `Shallow then freeze_invalid id ie;
-      Hooks.(call unreachable_state id ie);
+      Hooks.(call unreachable_state ~doc id ie);
       Exninfo.iraise ie
 
   let init_state = ref None
@@ -1072,7 +1073,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
   let is_filtered_command = function
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
-    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+    | VernacAbortAll | VernacAbort _ -> true
     | _ -> false
   in
   let aux_interp st expr =
@@ -1097,13 +1098,13 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
 module Backtrack : sig
 
   val record : unit -> unit
-  val backto : Stateid.t -> unit
 
   (* we could navigate the dag, but this ways easy *)
   val branches_of : Stateid.t -> backup
 
   (* Returns the state that the command should backtract to *)
-  val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when
+  val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when
+  val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
 
 end = struct (* {{{ *)
 
@@ -1122,14 +1123,6 @@ end = struct (* {{{ *)
       info.vcs_backup <- backup, branches)
     [VCS.current_branch (); VCS.Branch.master]
 
-  let backto oid =
-    let info = VCS.get_info oid in
-    match info.vcs_backup with
-    | None, _ ->
-       anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++
-               str": a state with no vcs_backup.")
-    | Some vcs, _ -> VCS.restore vcs
-
   let branches_of id =
     let info = VCS.get_info id in
     match info.vcs_backup with
@@ -1169,7 +1162,17 @@ end = struct (* {{{ *)
              " If your use is intentional, you may want to disable this warning and pass" ^
              " the \"-async-proofs-cache force\" option to Coq."))
 
-  let undo_vernac_classifier v =
+  let back_tactic n (id,_,_,tactic,undo) =
+    let value = (if tactic then 1 else 0) - undo in
+    if Int.equal n 0 then `Stop id else `Cont (n-value)
+
+  let get_proof ~doc id =
+    let open Vernacstate in
+    match state_of_id ~doc id with
+    | `Valid (Some vstate) -> Some (Proof_global.proof_of_state vstate.proof)
+    | _ -> None
+
+  let undo_vernac_classifier v ~doc =
     if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
@@ -1193,9 +1196,7 @@ end = struct (* {{{ *)
           oid, VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_,tactic,undo) ->
-            let value = (if tactic then 1 else 0) - undo in
-            if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
+          let oid = fold_until back_tactic n id in
           oid, VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
@@ -1220,7 +1221,6 @@ end = struct (* {{{ *)
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
           oid, VtLater
-      | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
           Stateid.of_int id, VtNow
       | _ -> anomaly Pp.(str "incorrect VtMeta classification")
@@ -1229,8 +1229,29 @@ end = struct (* {{{ *)
        CErrors.user_err ~hdr:"undo_vernac_classifier"
         Pp.(str "Cannot undo")
 
+  let get_prev_proof ~doc id =
+    try
+      let np = get_proof ~doc id in
+      match np with
+      | None -> None
+      | Some cp ->
+        let did = ref id in
+        let rv = ref np in
+        let done_ = ref false in
+        while not !done_ do
+          did := fold_until back_tactic 1 !did;
+          rv := get_proof ~doc !did;
+          done_ := match !rv with
+            | Some rv -> not (Goal.Set.equal (Proof.all_goals rv) (Proof.all_goals cp))
+            | None -> true
+        done;
+        !rv
+    with Not_found | Proof_global.NoCurrentProof -> None
+
 end (* }}} *)
 
+let get_prev_proof = Backtrack.get_prev_proof
+
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
@@ -1343,7 +1364,7 @@ module rec ProofTask : sig
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1362,6 +1383,7 @@ module rec ProofTask : sig
    and type request := request
 
   val build_proof_here :
+    doc:doc ->
     ?loc:Loc.t ->
     drop_pt:bool ->
     Stateid.t * Stateid.t -> Stateid.t ->
@@ -1381,7 +1403,7 @@ end = struct (* {{{ *)
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1476,11 +1498,12 @@ end = struct (* {{{ *)
         execution_error start (Pp.strbrk s);
         feedback (InProgress ~-1)
 
-  let build_proof_here ?loc ~drop_pt (id,valid) eop =
+  let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop =
     Future.create (State.exn_on id ~valid) (fun () ->
       let wall_clock1 = Unix.gettimeofday () in
-      if VCS.is_interactive () = `No then Reach.known_state ~cache:`No eop
-      else Reach.known_state ~cache:`Shallow eop;
+      if VCS.is_interactive () = `No
+      then Reach.known_state ~doc ~cache:`No eop
+      else Reach.known_state ~doc ~cache:`Shallow eop;
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at ?loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -1494,7 +1517,7 @@ end = struct (* {{{ *)
       VCS.print ();
       let proof, future_proof, time =
         let wall_clock = Unix.gettimeofday () in
-        let fp = build_proof_here ?loc ~drop_pt:drop exn_info stop in
+        let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in
         let proof = Future.force fp in
         proof, fp, Unix.gettimeofday () -. wall_clock in
       (* We typecheck the proof with the kernel (in the worker) to spot
@@ -1518,7 +1541,7 @@ end = struct (* {{{ *)
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in
+              expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1587,7 +1610,7 @@ end = struct (* {{{ *)
       msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
                              "The system state could not be sent to the worker process. "^
                              "Falling back to local, lazy, evaluation."));
-      t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop));
+      t_assign(`Comp(build_proof_here ~doc:dummy_doc (* XXX should be stored in a closure, it is the same doc that was used to generate the task *) ?loc:t_loc ~drop_pt t_exn_info t_stop));
       feedback (InProgress ~-1)
 
 end (* }}} *)
@@ -1597,6 +1620,7 @@ and Slaves : sig
 
   (* (eventually) remote calls *)
   val build_proof :
+    doc:doc ->
     ?loc:Loc.t -> drop_pt:bool ->
     exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t ->
       name:string -> future_proof * AsyncTaskQueue.cancel_switch
@@ -1644,7 +1668,7 @@ end = struct (* {{{ *)
         with VCS.Expired -> cur in
       aux stop in
     try
-      Reach.known_state ~cache:`No stop;
+      Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop;
       if drop then
         let _proof = Proof_global.return_proof ~allow_partial:true () in
         `OK_ADMITTED
@@ -1657,7 +1681,7 @@ end = struct (* {{{ *)
         Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
-      Reach.known_state ~cache:`No start;
+      Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start;
       (* STATE SPEC:
        * - start: First non-expired state! [This looks very fishy]
        * - end  : start + qed
@@ -1667,7 +1691,7 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
+          expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) });
       `OK proof
       end
     with e ->
@@ -1764,7 +1788,7 @@ end = struct (* {{{ *)
        BuildProof { t_states = s2 } -> overlap_rel s1 s2
      | _ -> 0)
 
-  let build_proof ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname =
+  let build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname =
     let id, valid as t_exn_info = exn_info in
     let cancel_switch = ref false in
     if TaskQueue.n_workers (Option.get !queue) = 0 then
@@ -1779,7 +1803,7 @@ end = struct (* {{{ *)
         TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch;
         f, cancel_switch
       end else
-        ProofTask.build_proof_here ?loc ~drop_pt t_exn_info block_stop, cancel_switch
+        ProofTask.build_proof_here ~doc ?loc ~drop_pt t_exn_info block_stop, cancel_switch
     else
       let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
@@ -1819,7 +1843,7 @@ and TacTask : sig
   type task = {
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
-    t_assign   : output Future.assignement -> unit;
+    t_assign   : output Future.assignment -> unit;
     t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
@@ -1836,7 +1860,7 @@ end = struct (* {{{ *)
   type task = {
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
-    t_assign   : output Future.assignement -> unit;
+    t_assign   : output Future.assignment -> unit;
     t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
@@ -1855,7 +1879,7 @@ end = struct (* {{{ *)
     | RespError of Pp.t
     | RespNoProgress
 
-  let name = ref "tacworker"
+  let name = ref "tacticworker"
   let extra_env () = [||]
   type competence = unit
   type worker_status = Fresh | Old of competence
@@ -1902,11 +1926,11 @@ end = struct (* {{{ *)
   let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
     Option.iter VCS.restore vcs;
     try
-      Reach.known_state ~cache:`No id;
+      Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id;
       stm_purify (fun () ->
        let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
-       let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in
+       let is_ground c = Evarutil.is_ground_term sigma0 c in
        if not (
          is_ground Evd.(evar_concl g) &&
          List.for_all (Context.Named.Declaration.for_all is_ground)
@@ -1929,7 +1953,6 @@ end = struct (* {{{ *)
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
-            let t = EConstr.of_constr t in
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               let t = EConstr.Unsafe.to_constr t in
@@ -2058,7 +2081,7 @@ end = struct (* {{{ *)
   let perform { r_where; r_doc; r_what; r_for } =
     VCS.restore r_doc;
     VCS.print ();
-    Reach.known_state ~cache:`No r_where;
+    Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where;
     (* STATE *)
     let st = Vernacstate.freeze_interp_state `No in
     try
@@ -2103,7 +2126,8 @@ end (* }}} *)
 and Reach : sig
 
   val known_state :
-    ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
+    doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable ->
+      Stateid.t -> unit
 
 end = struct (* {{{ *)
 
@@ -2119,12 +2143,6 @@ let delegate name =
   || VCS.is_vio_doc ()
   || !cur_opt.async_proofs_full
 
-let warn_deprecated_nested_proofs =
-  CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
-         (fun () ->
-          strbrk ("Nested proofs are deprecated and will "^
-                    "stop working in a future Coq version"))
-
 let collect_proof keep cur hd brkind id =
  stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
@@ -2133,7 +2151,7 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).loc in
  let is_defined_expr = function
-   | VernacEndProof (Proved (Transparent,_)) -> true
+   | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
    | _ -> false in
  let is_defined = function
    | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
@@ -2206,8 +2224,7 @@ let collect_proof keep cur hd brkind id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
         `MaybeASync (parent last, accn, name, delegate name)
-    | `Sideff _ ->
-       warn_deprecated_nested_proofs ();
+    | `Sideff (CherryPickEnv,_) ->
         `Sync (no_name,`NestedProof)
     | _ -> `Sync (no_name,`Unknown) in
  let make_sync why = function
@@ -2261,7 +2278,7 @@ let log_processing_sync id name reason = log_string Printf.(sprintf
 
 let wall_clock_last_fork = ref 0.0
 
-let known_state ?(redefine_qed=false) ~cache id =
+let known_state ~doc ?(redefine_qed=false) ~cache id =
 
   let error_absorbing_tactic id blockname exn =
     (* We keep the static/dynamic part of block detection separate, since
@@ -2294,7 +2311,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                Proof_global.unfreeze proof;
                Proof_global.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
-                 fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+                 fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
                (* STATE SPEC:
                 * - start: Modifies the input state adding a proof.
                 * - end  : maybe after recovery command.
@@ -2356,7 +2373,7 @@ let known_state ?(redefine_qed=false) ~cache id =
   and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
     stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
-      Hooks.(call state_computed id ~in_cache:true);
+      Hooks.(call state_computed ~doc id ~in_cache:true);
       stm_prerr_endline (fun () -> "reached (cache)");
       State.install_cached id
     end else
@@ -2437,7 +2454,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                         ^" proof. Reprocess the command declaring "
                         ^"the proof's statement to avoid that."));
                     let fp, cancel =
-                      Slaves.build_proof
+                      Slaves.build_proof ~doc
                         ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
                     Future.replace ofp fp;
                     qed.fproof <- Some (fp, cancel);
@@ -2449,10 +2466,10 @@ let known_state ?(redefine_qed=false) ~cache id =
                     reach ~cache:`Shallow block_start;
                     let fp, cancel =
                       if delegate then
-                        Slaves.build_proof
+                        Slaves.build_proof ~doc
                           ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
                       else
-                        ProofTask.build_proof_here ?loc
+                        ProofTask.build_proof_here ~doc ?loc
                           ~drop_pt exn_info block_stop, ref false
                     in
                     qed.fproof <- Some (fp, cancel);
@@ -2522,7 +2539,7 @@ let known_state ?(redefine_qed=false) ~cache id =
     let cache_step =
       if !cur_opt.async_proofs_cache = Some Force then `Yes
       else cache_step in
-    State.define ?safe_id
+    State.define ~doc ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
     stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
@@ -2571,8 +2588,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
 
   let load_objs libs =
     let rq_file (dir, from, exp) =
-      let mp = CAst.make @@ Libnames.(Qualid (qualid_of_string dir)) in
-      let mfrom = Option.map (fun fr -> CAst.make @@ Libnames.(Qualid (qualid_of_string fr))) from in
+      let mp = Libnames.qualid_of_string dir in
+      let mfrom = Option.map Libnames.qualid_of_string from in
       Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
     List.(iter rq_file (rev libs))
   in
@@ -2611,7 +2628,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   load_objs require_libs;
 
   (* We record the state at this point! *)
-  State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
+  State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
   if async_proofs_is_master !cur_opt then begin
@@ -2632,7 +2649,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
 let observe ~doc id =
   let vcs = VCS.backup () in
   try
-    Reach.known_state ~cache:(VCS.is_interactive ()) id;
+    Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
     VCS.print ();
     doc
   with e ->
@@ -2725,7 +2742,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname;
       VCS.delete_branch brname;
       VCS.gc ();
-      let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in
+      let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
@@ -2734,7 +2751,6 @@ let merge_proof_branch ~valid ?id qast keep brname =
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
 let handle_failure (e, info) vcs =
-  if e = CErrors.Drop then Exninfo.iraise (e, info) else
   match Stateid.get info with
   | None ->
       VCS.restore vcs;
@@ -2758,9 +2774,7 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
-  match part_of_script, w with
-  | true, w ->
+let process_back_meta_command ~newtip ~head oid aast w =
     let id = VCS.new_node ~id:newtip () in
     let { mine; others } = Backtrack.branches_of oid in
     let valid = VCS.get_branch_pos head in
@@ -2780,16 +2794,15 @@ let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
     VCS.commit id (Alias (oid,aast));
     Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
-  | false, VtNow ->
-    stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid);
-    Backtrack.backto oid;
-    VCS.checkout_shallowest_proof_branch ();
-    Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok
-
-  | false, VtLater ->
-    anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.")
+let allow_nested_proofs = ref false
+let _ = Goptions.declare_bool_option
+    { Goptions.optdepr  = false;
+      Goptions.optname  = "Nested Proofs Allowed";
+      Goptions.optkey   = Vernac_classifier.stm_allow_nested_proofs_option_name;
+      Goptions.optread  = (fun () -> !allow_nested_proofs);
+      Goptions.optwrite = (fun b -> allow_nested_proofs := b) }
 
-let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
+let process_transaction ~doc ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
@@ -2802,23 +2815,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
       match c with
       (* Meta *)
       | VtMeta, _ ->
-        let id, w = Backtrack.undo_vernac_classifier expr in
-        (* Special case Backtrack, as it is never part of a script. See #6240 *)
-        let part_of_script = begin match Vernacprop.under_control expr with
-          | VernacBacktrack _ -> false
-          | _ -> part_of_script
-        end in
-        process_back_meta_command ~part_of_script ~newtip ~head id x w
+        let id, w = Backtrack.undo_vernac_classifier expr ~doc in
+        process_back_meta_command ~newtip ~head id x w
+
       (* Query *)
-      | VtQuery (false,route), VtNow ->
-        let query_sid = VCS.cur_tip () in
-        (try
-           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
-           Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok
-      | VtQuery (true, route), w ->
+      | VtQuery, w ->
           let id = VCS.new_node ~id:newtip () in
           let queue =
             if !cur_opt.async_proofs_full then `QueryQueue (ref false)
@@ -2830,11 +2831,17 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
           VCS.commit id (mkTransCmd x [] false queue);
           Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
-      | VtQuery (false,_), VtLater ->
-          anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
-
       (* Proof *)
       | VtStartProof (mode, guarantee, names), w ->
+
+         if not !allow_nested_proofs && VCS.proof_nesting () > 0 then
+           "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
+           |> Pp.str
+           |> (fun s -> (UserError (None, s), Exninfo.null))
+           |> State.exn_on ~valid:Stateid.dummy Stateid.dummy
+           |> Exninfo.iraise
+         else
+
           let id = VCS.new_node ~id:newtip () in
           let bname = VCS.mk_branch_name x in
           VCS.checkout VCS.Branch.master;
@@ -2885,12 +2892,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
           Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
           rc
 
-      (* Side effect in a (still open) proof is replayed on all branches *)
-      | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop ->
-        let st = Vernacstate.freeze_interp_state `No in
-        ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
-        `Ok
-
+      (* Side effect in a (still open) proof is replayed on all branches*)
       | VtSideff l, w ->
           let id = VCS.new_node ~id:newtip () in
           begin match (VCS.get_branch head).VCS.kind with
@@ -2914,11 +2916,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
           let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
           let head_id = VCS.get_branch_pos head in
-          let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *)
+          let _st : unit = Reach.known_state ~doc ~cache:`Yes head_id in (* ensure it is ok *)
           let step () =
             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' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid 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 *)
@@ -2944,7 +2946,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
               end;
               VCS.checkout_shallowest_proof_branch ();
             end in
-          State.define ~safe_id:head_id ~cache:`Yes step id;
+          State.define ~doc ~safe_id:head_id ~cache:`Yes step id;
           Backtrack.record (); `Ok
 
       | VtUnknown, VtLater ->
@@ -3004,7 +3006,7 @@ let parse_sentence ~doc sid pa =
        str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
   Flags.with_option Flags.we_are_parsing (fun () ->
       try
-        match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+        match Pcoq.Entry.parse Pvernac.main_entry pa with
         | None            -> raise End_of_input
         | Some (loc, cmd) -> CAst.make ~loc cmd
       with e when CErrors.noncritical e ->
@@ -3058,7 +3060,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
   (* XXX: Classifiy vernac should be moved inside process transaction *)
   let clas = Vernac_classifier.classify_vernac ast in
   let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
-  match process_transaction ?newtip aast clas with
+  match process_transaction ~doc ?newtip aast clas with
   | `Ok -> doc, VCS.cur_tip (), `NewTip
   | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
 
@@ -3073,18 +3075,14 @@ type focus = {
 let query ~doc ~at ~route s =
   stm_purify (fun s ->
     if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
-    else Reach.known_state ~cache:`Yes at;
+    else Reach.known_state ~doc ~cache:`Yes at;
     try
       while true do
         let { CAst.loc; v=ast } = parse_sentence ~doc at s in
         let indentation, strlen = compute_indentation ?loc at in
-        let clas = Vernac_classifier.classify_vernac ast in
+        let st = State.get_cached at in
         let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
-        match clas with
-        | VtMeta , _ -> (* TODO: can this still happen ? *)
-          ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
-        | _ ->
-          ignore(process_transaction aast (VtQuery (false,route), VtNow))
+        ignore(stm_vernac_interp ~route at st aast)
       done;
     with
     | End_of_input -> ()
@@ -3139,7 +3137,7 @@ let edit_at ~doc id =
       VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
     VCS.delete_boxes_of id;
     cancel_switch := true;
-    Reach.known_state ~cache:(VCS.is_interactive ()) id;
+    Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `Focus { stop = qed_id; start = master_id; tip } in
   let no_edit = function
@@ -3162,7 +3160,7 @@ let edit_at ~doc id =
     VCS.gc ();
     VCS.print ();
     if not !cur_opt.async_proofs_full then
-      Reach.known_state ~cache:(VCS.is_interactive ()) id;
+      Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
@@ -3191,7 +3189,7 @@ let edit_at ~doc id =
       | true, None, _ ->
           if on_cur_branch id then begin
             VCS.reset_branch (VCS.current_branch ()) id;
-            Reach.known_state ~cache:(VCS.is_interactive ()) id;
+            Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
             VCS.checkout_shallowest_proof_branch ();
             `NewTip
           end else if is_ancestor_of_cur_branch id then begin
diff --git a/stm/stm.mli b/stm/stm.mli
index 35ce77a3..1e5ceb7e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -92,11 +92,11 @@ val new_doc  : stm_init_options -> doc * Stateid.t
 
 (** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
+val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t ->
   Vernacexpr.vernac_control CAst.t
 
 (* Reminder: A parsable [pa] is constructed using
-   [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
+   [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
 
 exception End_of_input
 
@@ -110,11 +110,16 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
   bool -> Vernacexpr.vernac_control CAst.t ->
   doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
+(* Returns the proof state before the last tactic that was applied at or before
+the specified state AND that has differences in the underlying proof (i.e.,
+ignoring proofview-only changes).  Used to compute proof diffs. *)
+val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],
    throwing away side effects except messages. Feedback will
    be sent with [report_with], which defaults to the dummy state id *)
 val query : doc:doc ->
-  at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit
+  at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit
 
 (* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
    the requested id is the new document tip hence the document portion following
@@ -263,11 +268,12 @@ val register_proof_block_delimiter :
  * the alternative toploop for the worker can be selected by changing
  * the name of the Task(s) above) *)
 
-val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
-val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
+val state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t
+val unreachable_state_hook :
+  (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t
 
 (* ready means that master has it at hand *)
-val state_ready_hook : (Stateid.t -> unit) Hook.t
+val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t
 
 (* Messages from the workers to the master *)
 val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 72b53801..4b254e81 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -5,7 +5,6 @@ TQueue
 WorkerPool
 Vernac_classifier
 CoqworkmgrApi
-WorkerLoop
 AsyncTaskQueue
 Stm
 ProofBlockDelimiter
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
deleted file mode 100644
index 3b91df86..00000000
--- a/stm/tacworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
-
-let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-
-let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
-
diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib
deleted file mode 100644
index db38fde2..00000000
--- a/stm/tacworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Tacworkertop
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f68c8b32..21704779 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -16,8 +16,6 @@ open Vernacexpr
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
 
-let string_of_in_script b = if b then " (inside script)" else ""
-
 let string_of_parallel = function
   | `Yes (solve,abs) ->
        "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -34,7 +32,7 @@ let string_of_vernac_type = function
       "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
-  | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+  | VtQuery -> "Query"
   | VtMeta -> "Meta "
 
 let string_of_vernac_when = function
@@ -44,25 +42,25 @@ let string_of_vernac_when = function
 let string_of_vernac_classification (t,w) =
   string_of_vernac_type t ^ " " ^ string_of_vernac_when w
 
-let classifiers = ref []
-let declare_vernac_classifier
-  (s : Vernacexpr.extend_name)
-  (f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
-=
-  classifiers := !classifiers @ [s,f]
-
 let idents_of_name : Names.Name.t -> Names.Id.t list =
   function
   | Names.Anonymous -> []
   | Names.Name n -> [n]
 
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+  [ Vernacentries.universe_polymorphism_option_name;
+    stm_allow_nested_proofs_option_name ]
+
 let classify_vernac e =
   let static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
     | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
-      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+      when CList.exists (CList.equal String.equal l)
+        options_affecting_stm_scheduling ->
        VtSideff [], VtNow
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
@@ -70,7 +68,7 @@ let classify_vernac e =
     | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
+    | VernacCheckMayEval _ -> VtQuery, VtLater
     (* ProofStep *)
     | VernacProof _ 
     | VernacFocus _ | VernacUnfocus
@@ -145,7 +143,7 @@ let classify_vernac e =
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
     | VernacChdir _ 
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
-    | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+    | VernacArguments _
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
@@ -157,6 +155,7 @@ let classify_vernac e =
     | VernacDeclareClass _ | VernacDeclareInstances _
     | VernacRegister _
     | VernacNameSectionHypSet _
+    | VernacDeclareCustomEntry _
     | VernacComments _ -> VtSideff [], VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
@@ -183,30 +182,26 @@ let classify_vernac e =
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+    | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
     (* What are these? *)
-    | VernacToplevelControl _
     | VernacRestoreState _
     | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
-        try List.assoc s !classifiers l ()
+        try Vernacentries.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let poly = List.fold_left (fun poly f ->
-          match f with
-          | VernacPolymorphic b -> b
-          | (VernacProgram | VernacLocal _) -> poly
-        ) poly f in
+      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
+      let poly = atts.Vernacinterp.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
        static_control_classifier ~poly e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier ~poly e with
-        | ( VtQuery _ | VtProofStep _ | VtSideff _
+        | ( VtQuery | VtProofStep _ | VtSideff _
           | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
@@ -215,6 +210,6 @@ let classify_vernac e =
   in
   static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
 
-let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
+let classify_as_query = VtQuery, VtLater
 let classify_as_sideeff = VtSideff [], VtLater
 let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index abbc04e8..e82b1914 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -9,19 +9,15 @@
 (************************************************************************)
 
 open Vernacexpr
-open Genarg
 
 val string_of_vernac_classification : vernac_classification -> string
 
 (** What does a vernacular do *)
 val classify_vernac : vernac_control -> vernac_classification
 
-(** Install a vernacular classifier for VernacExtend *)
-val declare_vernac_classifier :
-  Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
-
 (** Standard constant classifiers *)
 val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
 val classify_as_proofstep : vernac_classification
 
+val stm_allow_nested_proofs_option_name : string list
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
deleted file mode 100644
index 5445925b..00000000
--- a/stm/workerLoop.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Default priority *)
-open CoqworkmgrApi
-let async_proofs_worker_priority = ref Low
-
-let rec parse = function
-  | "--xml_format=Ppcmds" :: rest -> parse rest
-  | x :: rest -> x :: parse rest
-  | [] -> []
-
-let loop init _coq_args extra_args =
-  let args = parse extra_args in
-  Flags.quiet := true;
-  init ();
-  CoqworkmgrApi.init !async_proofs_worker_priority;
-  args
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
deleted file mode 100644
index f02edb9b..00000000
--- a/stm/workerLoop.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Default priority *)
-val async_proofs_worker_priority : CoqworkmgrApi.priority ref
-
-val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list