Imported Upstream version 8.8.2upstream/8.8.2

30 files changed, 1879 insertions, 1942 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index fa6422cd..b3e1500a 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -1,26 +1,30 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 open CErrors
 open Pp
 open Util
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
 
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
-
-type 'a worker_status = [ `Fresh | `Old of 'a ]
+type cancel_switch = bool ref
+let async_proofs_flags_for_workers = ref []
 
 module type Task = sig
 
   type task
   type competence
 
+  type worker_status = Fresh | Old of competence
+
   (* Marshallable *)
   type request
   type response
@@ -29,15 +33,14 @@ module type Task = sig
   val extra_env : unit -> string array
 
   (* run by the master, on a thread *)
-  val request_of_task : competence worker_status -> task -> request option
-  val task_match : competence worker_status -> task -> bool
-  val use_response :
-    competence worker_status -> task -> response ->
-      [ `Stay of competence * task list | `End ]
+  val request_of_task : worker_status -> task -> request option
+  val task_match : worker_status -> task -> bool
+  val use_response : worker_status -> task -> response ->
+    [ `Stay of competence * task list | `End ]
   val on_marshal_error : string -> task -> unit
   val on_task_cancellation_or_expiration_or_slave_death : task option -> unit
   val forward_feedback : Feedback.feedback -> unit
- 
+
   (* run by the worker *)
   val perform : request -> response
 
@@ -47,9 +50,7 @@ module type Task = sig
 
 end
 
-type expiration = bool ref
-
-module Make(T : Task) = struct
+module Make(T : Task) () = struct
 
   exception Die
   type response =
@@ -59,45 +60,45 @@ module Make(T : Task) = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of Univ.universe_level list
+    | MoreDataUnivLevel of Universes.universe_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in
     Response res
 
   exception MarshalError of string
-  
+
   let marshal_to_channel oc data =
     Marshal.to_channel oc data [];
     flush oc
-  
+
   let marshal_err s = raise (MarshalError s)
-  
+
   let marshal_request oc (req : request) =
     try marshal_to_channel oc req
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("marshal_request: "^s)
-  
+
   let unmarshal_request ic =
     try (CThread.thread_friendly_input_value ic : request)
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("unmarshal_request: "^s)
-  
+
   let marshal_response oc (res : response) =
     try marshal_to_channel oc res
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("marshal_response: "^s)
-  
+
   let unmarshal_response ic =
     try (CThread.thread_friendly_input_value ic : response)
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("unmarshal_response: "^s)
-  
+
   let marshal_more_data oc (res : more_data) =
     try marshal_to_channel oc res
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("marshal_more_data: "^s)
-  
+
   let unmarshal_more_data ic =
     try (CThread.thread_friendly_input_value ic : more_data)
     with Failure s | Invalid_argument s | Sys_error s ->
@@ -105,24 +106,24 @@ module Make(T : Task) = struct
 
   let report_status ?(id = !Flags.async_proofs_worker_id) s =
     let open Feedback in
-    feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
+    feedback ~id:Stateid.initial (WorkerStatus(id, s))
 
-  module Worker = Spawn.Sync(struct end)
+  module Worker = Spawn.Sync ()
 
   module Model = struct
 
   type process = Worker.process
-  type extra = (T.task * expiration) TQueue.t
+  type extra = (T.task * cancel_switch) TQueue.t
 
   let spawn id =
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
       let rec set_slave_opt = function
-        | [] -> !Flags.async_proofs_flags_for_workers @
+        | [] -> !async_proofs_flags_for_workers @
                 ["-toploop"; !T.name^"top";
                  "-worker-id"; name;
                  "-async-proofs-worker-priority";
-                   Flags.string_of_priority !Flags.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"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
@@ -140,38 +141,37 @@ module Make(T : Task) = struct
     let { WorkerPool.extra = queue; exit; cancelled } = cpanel in
     let exit () =  report_status ~id "Dead"; exit () in
     let last_task = ref None in
-    let worker_age = ref `Fresh in
+    let worker_age = ref T.Fresh in
     let got_token = ref false in
     let giveback_exec_token () =
       if !got_token then (CoqworkmgrApi.giveback 1; got_token := false) in
     let stop_waiting = ref false in
     let expiration_date = ref (ref false) in
     let pick_task () =
-      prerr_endline "waiting for a task";
+      stm_prerr_endline "waiting for a task";
       let pick age (t, c) = not !c && T.task_match age t in
       let task, task_expiration =
         TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
       expiration_date := task_expiration;
       last_task := Some task;
-      prerr_endline ("got task: "^T.name_of_task task);
+      stm_prerr_endline ("got task: " ^ T.name_of_task task);
       task in
     let add_tasks l =
       List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
     let get_exec_token () =
       ignore(CoqworkmgrApi.get 1);
       got_token := true;
-      prerr_endline ("got execution token") in
+      stm_prerr_endline ("got execution token") in
     let kill proc =
       Worker.kill proc;
-      prerr_endline ("Worker exited: " ^
+      stm_prerr_endline ("Worker exited: " ^
         match Worker.wait proc with
         | Unix.WEXITED 0x400 -> "exit code unavailable"
         | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
     let more_univs n =
-      CList.init 10 (fun _ ->
-        Universes.new_univ_level (Global.current_dirpath ())) in
+      CList.init n (fun _ -> Universes.new_univ_id ()) in
 
     let rec kill_if () =
       if not (Worker.is_alive proc) then ()
@@ -196,7 +196,7 @@ module Make(T : Task) = struct
       report_status ~id "Idle";
       let task = pick_task () in
       match T.request_of_task !worker_age task with
-      | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+      | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task)
       | Some req ->
       try
         get_exec_token ();
@@ -213,7 +213,7 @@ module Make(T : Task) = struct
               | `Stay(competence, new_tasks) ->
                    last_task := None;
                    giveback_exec_token ();
-                   worker_age := `Old competence;
+                   worker_age := T.Old competence;
                    add_tasks new_tasks
         in
           continue ()
@@ -222,8 +222,7 @@ module Make(T : Task) = struct
           raise e (* we pass the exception to the external handler *)
       | MarshalError s -> T.on_marshal_error s task; raise Die
       | e ->
-          pr_err ("Uncaught exception in worker manager: "^
-            string_of_ppcmds (print e));
+          stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
           flush_all (); raise Die
     done with
     | (Die | TQueue.BeingDestroyed) ->
@@ -237,8 +236,8 @@ module Make(T : Task) = struct
 
   type queue = {
     active : Pool.pool;
-    queue : (T.task * expiration) TQueue.t;
-    cleaner : Thread.t;
+    queue : (T.task * cancel_switch) TQueue.t;
+    cleaner : Thread.t option;
   }
 
   let create size =
@@ -251,18 +250,18 @@ module Make(T : Task) = struct
     {
       active = Pool.create queue ~size;
       queue;
-      cleaner = Thread.create cleaner queue;
+      cleaner = if size > 0 then Some (Thread.create cleaner queue) else None;
     }
-  
+
   let destroy { active; queue } =
     Pool.destroy active;
     TQueue.destroy queue
 
   let broadcast { queue } = TQueue.broadcast queue
 
-  let enqueue_task { queue; active } (t, _ as item) =
-    prerr_endline ("Enqueue task "^T.name_of_task t);
-    TQueue.push queue item
+  let enqueue_task { queue; active } t ~cancel_switch =
+    stm_prerr_endline ("Enqueue task "^T.name_of_task t);
+    TQueue.push queue (t, cancel_switch)
 
   let cancel_worker { active } n = Pool.cancel n active
 
@@ -298,28 +297,20 @@ module Make(T : Task) = struct
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
-  let pp_pid pp = 
-    (* Breaking all abstraction barriers... very nice *)
-    let get_xml pp = match Richpp.repr pp with
-      | Xml_datatype.Element("_", [], xml) -> xml
-      | _ -> assert false in
-    Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
-      get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
-      get_xml pp))
+  let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp)
 
   let debug_with_pid = Feedback.(function
     | { contents = Message(Debug, loc, pp) } as fb ->
-       { fb with contents = Message(Debug,loc,pp_pid pp) }
+       { fb with contents = Message(Debug,loc, pp_pid pp) }
     | x -> x)
 
   let main_loop () =
     (* We pass feedback to master *)
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
-    Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Feedback.set_logger Feedback.feedback_logger;
+    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_level (bufferize (fun () ->
+    Universes.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));
@@ -337,25 +328,25 @@ module Make(T : Task) = struct
         CEphemeron.clear ()
       with
       | MarshalError s ->
-        pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+        stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
       | End_of_file ->
-        prerr_endline "connection lost"; flush_all (); exit 2
+        stm_prerr_endline "connection lost"; flush_all (); exit 2
       | e ->
-        pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+        stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
         flush_all (); exit 1
     done
 
   let clear { queue; active } =
     assert(Pool.is_empty active); (* We allow that only if no slaves *)
     TQueue.clear queue
-  
+
   let snapshot { queue; active } =
     List.map fst
      (TQueue.wait_until_n_are_waiting_then_snapshot
        (Pool.n_workers active) queue)
 
   let with_n_workers n f =
-    let q = create n in 
+    let q = create n in
     try let rc = f q in destroy q; rc
     with e -> let e = CErrors.push e in destroy q; iraise e
 
@@ -363,5 +354,5 @@ module Make(T : Task) = struct
 
 end
 
-module MakeQueue(T : Task) = struct include Make(T) end
-module MakeWorker(T : Task) = struct include Make(T) end
+module MakeQueue(T : Task) () = struct include Make(T) () end
+module MakeWorker(T : Task) () = struct include Make(T) () end
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index f140f8ed..6e6827c7 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -1,84 +1,221 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
-type 'a worker_status = [ `Fresh | `Old of 'a ]
+(* Default flags for workers *)
+val async_proofs_flags_for_workers : string list ref
 
+(** This file provides an API for defining and managing a queue of
+    tasks to be done by external workers.
+
+    A queue of items of type [task] is maintained, then for each task,
+    a request is generated, then sent to a worker using marshalling.
+
+    The workers will then eventually return a result, using marshalling
+    again:
+     ____ ____ ____                    ________
+    | T1 | T2 | T3 | => [request ] => | Worker |
+    |____|____|____| <= [response] <= |________|
+    | Master Proc. |
+    \--------------/
+
+    Thus [request] and [response] must be safely marshallable.
+
+    Operations for managing the task queue are provide, see below
+    for more details.
+
+ *)
+
+(** The [Task] module type defines an abstract message-processing
+    queue. *)
 module type Task = sig
 
+  (** Main description of a task. Elements are stored in the "master"
+      process, and then converted into a request.
+  *)
   type task
+
+  (** [competence] stores the information about what kind of work a
+      worker has completed / has available. *)
   type competence
 
-  (* Marshallable *)
+  (** A worker_status is:
+
+    - [`Fresh] when a worker is born.
+
+    - [`Old of competence]: When a worker ends a job it can either die
+      (and be replaced by a fresh new worker) or hang there as an [`Old]
+      worker. In such case some data can be carried by the [`Old]
+      constructor, typically used to implement [request_of_task].
+
+      This allows to implement both one-shot workers and "persistent"
+      ones. E.g. par: is implement using workers that don't
+      "reboot". Proof workers do reboot mainly because the vm has some
+      C state that cannot be cleared, so you have a real memory leak if
+      you don't reboot the worker. *)
+  type worker_status = Fresh | Old of competence
+
+  (** Type of input and output data for workers.
+
+      The data must be marshallable as it send through the network
+      using [Marshal] . *)
   type request
   type response
 
-  val name : string ref (* UID of the task kind, for -toploop *)
+  (** UID of the task kind, for -toploop *)
+  val name : string ref
+  (** Extra arguments of the task kind, for -toploop *)
   val extra_env : unit -> string array
 
-  (* run by the master, on a thread *)
-  val request_of_task : competence worker_status -> task -> request option
-  val task_match : competence worker_status -> task -> bool
-  val use_response :
-    competence worker_status -> task -> response ->
-      [ `Stay of competence * task list | `End ]
+  (** {5 Master API, it is run by the master, on a thread} *)
+
+  (** [request_of_task status t] takes the [status] of the worker
+      and a task [t] and creates the corresponding [Some request] to be
+      sent to the worker or it is not valid anymore [None]. *)
+  val request_of_task : worker_status -> task -> request option
+
+  (** [task_match status tid] Allows to discard tasks based on the
+      worker status.  *)
+  val task_match : worker_status -> task -> bool
+
+  (** [use_response status t out]
+
+      For a response [out] to a task [t] with [status] we can choose
+      to end the worker of to keep it alive with some data and
+      immediately inject extra tasks in the queue.
+
+      For example, the proof worker runs a proof and finds an error,
+      the response signals that, e.g.
+
+      [ReponseError {state = 34; msg = "oops"}]
+
+      When the manager uses such a response he can tell the worker to
+      stay there and inject into the queue an extra task requesting
+      state 33 (to implement efficient proof repair).  *)
+  val use_response : worker_status -> task -> response ->
+    [ `Stay of competence * task list | `End ]
+
+  (** [on_marshal_error err_msg tid] notifies of marshaling failure. *)
   val on_marshal_error : string -> task -> unit
+
+  (** [on_task_cancellation_or_expiration_or_slave_death tid]
+
+      These functions are meant to parametrize the worker manager on
+      the actions to be taken when things go wrong or are cancelled
+      (you can kill a worker in CoqIDE, or using kill -9...)
+
+      E.g. master can decide to inhabit the (delegate) Future.t with a
+      closure (to be run in master), i.e. make the document still
+      checkable. This is what I do for marshaling errors.  *)
   val on_task_cancellation_or_expiration_or_slave_death : task option -> unit
+
+  (** [forward_feedback fb] sends fb to all the workers. *)
   val forward_feedback : Feedback.feedback -> unit
- 
-  (* run by the worker *)
+
+  (** {5 Worker API, it is run by worker, on a different fresh
+      process} *)
+
+  (** [perform in] synchronously processes a request [in] *)
   val perform : request -> response
 
-  (* debugging *)
+  (** debugging *)
   val name_of_task : task -> string
   val name_of_request : request -> string
 
 end
 
-type expiration = bool ref
+(** [cancel_switch] to be flipped to true by anyone to signal the task
+    is not relevant anymore. When the STM performs an undo/edit-at, it
+    crawls the document and flips these flags (the Qed node carries a
+    pointer to the flag IIRC).
+*)
+type cancel_switch = bool ref
 
-module MakeQueue(T : Task) : sig
+(** Client-side functor. [MakeQueue T] creates a task queue for task [T]  *)
+module MakeQueue(T : Task) () : sig
 
+  (** [queue] is the abstract queue type. *)
   type queue
 
-  (* Number of workers, 0 = lazy local *)
+  (** [create n] will initialize the queue with [n] workers. If [n] is
+      0, the queue won't spawn any process, working in a lazy local
+      manner. [not imposed by the this API] *)
   val create : int -> queue
+
+  (** [destroy q] Deallocates [q], cancelling all pending tasks. *)
   val destroy : queue -> unit
 
+  (** [n_workers q] returns the number of workers of [q] *)
   val n_workers : queue -> int
 
-  val enqueue_task : queue -> T.task * expiration -> unit
+  (** [enqueue_task q t ~cancel_switch] schedules [t] for execution in
+      [q]. [cancel_switch] can be flipped to true to cancel the task. *)
+  val enqueue_task : queue -> T.task -> cancel_switch:cancel_switch -> unit
 
-  (* blocking function that waits for the task queue to be empty *)
+  (** [join q] blocks until the task queue is empty *)
   val join : queue -> unit
+
+  (** [cancel_all q] Cancels all tasks *)
   val cancel_all : queue -> unit
 
+  (** [cancel_worker q wid] cancels a particular worker [wid] *)
   val cancel_worker : queue -> WorkerPool.worker_id -> unit
 
+  (** [set_order q cmp] reorders [q] using ordering [cmp] *)
   val set_order : queue -> (T.task -> T.task -> int) -> unit
 
+  (** [broadcast q]
+
+      This is nasty. Workers can be picky, e.g. pick tasks only when
+      they are "on screen". Of course the screen is scrolled, and that
+      changes the potential choice of workers to pick up a task or
+      not.
+
+      This function wakes up the workers (the managers) that give a
+      look (again) to the tasks in the queue.
+
+      The STM calls it when the perspective (as in PIDE) changes.
+
+      A problem here is that why task_match has access to the
+      competence data in order to decide if the task is palatable to
+      the worker or not... such data is local to the worker (manager).
+      The perspective is global, so it does not quite fit this
+      picture. This API to make all managers reconsider the tasks in
+      the queue is the best I could came up with.
+
+      This API is crucial to Coqoon (or any other UI that invokes
+      Stm.finish eagerly but wants the workers to "focus" on the visible
+      part of the document).
+  *)
   val broadcast : queue -> unit
 
-  (* Take a snapshot (non destructive but waits until all workers are
-   * enqueued) *)
+  (** [snapshot q] Takes a snapshot (non destructive but waits until
+      all workers are enqueued) *)
   val snapshot : queue -> T.task list
 
-  (* Clears the queue, only if the worker prool is empty *)
- val clear : queue -> unit
- 
-  (* create a queue, run the function, destroy the queue.
-   * the user should call join *)
+  (** [clear q] Clears [q], only if the worker prool is empty *)
+  val clear : queue -> unit
+
+  (** [with_n_workers n f] create a queue, run the function, destroy
+      the queue. The user should call join *)
   val with_n_workers : int -> (queue -> 'a) -> 'a
 
 end
 
-module MakeWorker(T : Task) : sig
+(** Server-side functor. [MakeWorker T] creates the server task
+    dispatcher. *)
+module MakeWorker(T : Task) () : sig
 
-  val main_loop : unit -> unit
+  (** [init_stdout ()] is called at [Coqtop.toploop_init] time. *)
   val init_stdout : unit -> unit
-  
+
+  (** [main_loop ()] is called at [Coqtop.toploop_run] time. *)
+  val main_loop : unit -> unit
+
 end
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 20d5152a..36b5d18a 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -1,15 +1,24 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 let debug = false
 
+type priority = Low | High
+let string_of_priority = function Low -> "low" | High -> "high"
+let priority_of_string = function
+  | "low" -> Low
+  | "high" -> High
+  | _ -> raise (Invalid_argument "priority_of_string")
+
 type request =
-  | Hello of Flags.priority
+  | Hello of priority
   | Get of int
   | TryGet of int
   | GiveBack of int
@@ -36,8 +45,8 @@ let positive_int_of_string n =
 let parse_request s =
   if debug then Printf.eprintf "parsing '%s'\n" s;
   match Str.split (Str.regexp " ") (strip_r s) with
-  | [ "HELLO"; "LOW" ] -> Hello Flags.Low
-  | [ "HELLO"; "HIGH" ] -> Hello Flags.High
+  | [ "HELLO"; "LOW" ] -> Hello Low
+  | [ "HELLO"; "HIGH" ] -> Hello High
   | [ "GET"; n ] -> Get (positive_int_of_string n)
   | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n)
   | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n)
@@ -57,8 +66,8 @@ let parse_response s =
   | _ -> raise ParseError
        
 let print_request = function
-  | Hello Flags.Low -> "HELLO LOW\n"
-  | Hello Flags.High -> "HELLO HIGH\n"
+  | Hello Low -> "HELLO LOW\n"
+  | Hello High -> "HELLO HIGH\n"
   | Get n -> Printf.sprintf "GET %d\n" n
   | TryGet n -> Printf.sprintf "TRYGET %d\n" n
   | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n
@@ -106,8 +115,7 @@ let with_manager f g =
 
 let get n =
   with_manager
-  (fun () ->
-    min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))
+  (fun () -> n)
   (fun cin cout ->
     output_string cout (print_request (Get n));
     flush cout;
@@ -118,10 +126,7 @@ let get n =
 
 let tryget n =
   with_manager
-  (fun () ->
-    Some
-     (min n
-       (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)))
+  (fun () -> Some n)
   (fun cin cout ->
     output_string cout (print_request (TryGet n));
     flush cout;
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 54895814..2983b619 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -1,16 +1,22 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* High level api for clients of the service (like coqtop) *)
 
+type priority = Low | High
+val string_of_priority : priority -> string
+val priority_of_string : string -> priority
+
 (* Connects to a work manager if any. If no worker manager, then
    -async-proofs-j and -async-proofs-tac-j are used *)
-val init : Flags.priority -> unit
+val init : priority -> unit
 
 (* blocking *)
 val get : int -> int
@@ -21,7 +27,7 @@ val giveback : int -> unit
 
 (* Low level *)
 type request =
-  | Hello of Flags.priority
+  | Hello of priority
   | Get of int
   | TryGet of int
   | GiveBack of int
diff --git a/stm/dag.ml b/stm/dag.ml
index 99e7c926..eb5063bf 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 type S = sig
diff --git a/stm/dag.mli b/stm/dag.mli
index e783cd8e..cae4fccc 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 type S = sig
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
deleted file mode 100644
index 022c89ad..00000000
--- a/stm/lemmas.ml
+++ /dev/null
@@ -1,555 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Created by Hugo Herbelin from contents related to lemma proofs in
-   file command.ml, Aug 2009 *)
-
-open CErrors
-open Util
-open Flags
-open Pp
-open Names
-open Term
-open Declarations
-open Declareops
-open Entries
-open Environ
-open Nameops
-open Globnames
-open Decls
-open Decl_kinds
-open Declare
-open Pretyping
-open Termops
-open Namegen
-open Reductionops
-open Constrexpr
-open Constrintern
-open Impargs
-open Context.Rel.Declaration
-
-type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
-let mk_hook hook = hook
-let call_hook fix_exn hook l c =
-  try hook l c
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    iraise (fix_exn e)
-
-(* Support for mutually proved theorems *)
-
-let retrieve_first_recthm = function
-  | VarRef id ->
-      let open Context.Named.Declaration in
-      (get_value (Global.lookup_named id),variable_opacity id)
-  | ConstRef cst ->
-      let cb = Global.lookup_constant cst in
-      (Global.body_of_constant_body cb, is_opaque cb)
-  | _ -> assert false
-
-let adjust_guardness_conditions const = function
-  | [] -> const (* Not a recursive statement *)
-  | possible_indexes ->
-  (* Try all combinations... not optimal *)
-     let env = Global.env() in
-     { const with const_entry_body =
-        Future.chain ~greedy:true ~pure:true const.const_entry_body
-        (fun ((body, ctx), eff) ->
-          match kind_of_term body with
-          | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-(*      let possible_indexes =
-	List.map2 (fun i c -> match i with Some i -> i | None ->
-	  List.interval 0 (List.length ((lam_assum c))))
-	  lemma_guard (Array.to_list fixdefs) in
-*)
-              let add c cb e =
-                let exists c e =
-                  try ignore(Environ.lookup_constant c e); true
-                  with Not_found -> false in 
-                if exists c e then e else Environ.add_constant c cb e in
-              let env = List.fold_left (fun env { eff } ->
-                match eff with
-                | SEsubproof (c, cb,_) -> add c cb env
-                | SEscheme (l,_) ->
-                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
-                env (Safe_typing.side_effects_of_private_constants eff) in
-              let indexes =
-                search_guard Loc.ghost env
-                  possible_indexes fixdecls in
-		(mkFix ((indexes,0),fixdecls), ctx), eff
-          | _ -> (body, ctx), eff) }
-
-let find_mutually_recursive_statements thms =
-    let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls,annot)) ->
-      let (hyps,ccl) = decompose_prod_assum t in
-      let x = (id,(t,impls)) in
-      match annot with
-      (* Explicit fixpoint decreasing argument is given *)
-      | Some (Some (_,id),CStructRec) ->
-          let i,b,typ = lookup_rel_id id hyps in
-          (match kind_of_term t with
-          | Ind ((kn,_ as ind), u) when
-              let mind = Global.lookup_mind kn in
-              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
-              [ind,x,i],[]
-          | _ ->
-              error "Decreasing argument is not an inductive assumption.")
-      (* Unsupported cases *)
-      | Some (_,(CWfRec _|CMeasureRec _)) ->
-          error "Only structural decreasing is supported for mutual statements."
-      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
-      | None | Some (None, CStructRec) ->
-      let whnf_hyp_hds = map_rel_context_in_env
-        (fun env c -> fst (whd_all_stack env Evd.empty c))
-        (Global.env()) hyps in
-      let ind_hyps =
-        List.flatten (List.map_i (fun i decl ->
-          let t = get_type decl in
-          match kind_of_term t with
-          | Ind ((kn,_ as ind),u) when
-                let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
-              [ind,x,i]
-          | _ ->
-              []) 0 (List.rev whnf_hyp_hds)) in
-      let ind_ccl =
-        let cclenv = push_rel_context hyps (Global.env()) in
-        let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
-        match kind_of_term whnf_ccl with
-        | Ind ((kn,_ as ind),u) when
-              let mind = Global.lookup_mind kn in
-              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
-            [ind,x,0]
-        | _ ->
-            [] in
-      ind_hyps,ind_ccl) thms in
-    let inds_hyps,ind_ccls = List.split inds in
-    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
-    (* Check if all conclusions are coinductive in the same type *)
-    (* (degenerated cartesian product since there is at most one coind ccl) *)
-    let same_indccl =
-      List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] ind_ccls in
-    let ordered_same_indccl =
-      List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
-    (* Check if some hypotheses are inductive in the same type *)
-    let common_same_indhyp =
-      List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] inds_hyps in
-    let ordered_inds,finite,guard =
-      match ordered_same_indccl, common_same_indhyp with
-      | indccl::rest, _ ->
-	  assert (List.is_empty rest);
-          (* One occ. of common coind ccls and no common inductive hyps *)
-	  if not (List.is_empty common_same_indhyp) then
-	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
-	  flush_all ();
-          indccl, true, []
-      | [], _::_ ->
-          let () = match same_indccl with
-          | ind :: _ ->
-            if List.distinct_f ind_ord (List.map pi1 ind)
-            then
-              if_verbose Feedback.msg_info
-                (strbrk
-                   ("Coinductive statements do not follow the order of "^
-                    "definition, assuming the proof to be by induction."));
-            flush_all ()
-          | _ -> ()
-          in
-          let possible_guards = List.map (List.map pi3) inds_hyps in
-	  (* assume the largest indices as possible *)
-	  List.last common_same_indhyp, false, possible_guards
-      | _, [] ->
-	  error
-            ("Cannot find common (mutual) inductive premises or coinductive" ^
-             " conclusions in the statements.")
-    in
-    (finite,guard,None), ordered_inds
-
-let look_for_possibly_mutual_statements = function
-  | [id,(t,impls,None)] ->
-      (* One non recursively proved theorem *)
-      None,[id,(t,impls)],None
-  | _::_ as thms ->
-    (* More than one statement and/or an explicit decreasing mark: *)
-    (* we look for a common inductive hyp or a common coinductive conclusion *)
-    let recguard,ordered_inds = find_mutually_recursive_statements thms in
-    let thms = List.map pi2 ordered_inds in
-    Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
-  | [] -> anomaly (Pp.str "Empty list of theorems.")
-
-(* Saving a goal *)
-
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
-  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
-  try
-    let const = adjust_guardness_conditions const do_guard in
-    let k = Kindops.logical_kind_of_goal_kind kind in
-    let l,r = match locality with
-      | Discharge when Lib.sections_are_opened () ->
-          let c = SectionLocalDef const in
-          let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Local, VarRef id)
-      | Local | Global | Discharge ->
-          let local = match locality with
-          | Local | Discharge -> true
-          | Global -> false
-          in
-          let kn =
-           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
-          (locality, ConstRef kn) in
-    definition_message id;
-    Option.iter (Universes.register_universe_binders r) pl;
-    call_hook (fun exn -> exn) hook l r
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    iraise (fix_exn e)
-
-let default_thm_id = Id.of_string "Unnamed_thm"
-
-let compute_proof_name locality = function
-  | Some ((loc,id),pl) ->
-      (* We check existence here: it's a bit late at Qed time *)
-      if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
-	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
-      then
-        user_err_loc (loc,"",pr_id id ++ str " already exists.");
-      id, pl
-  | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
-
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
-  let t_i = norm t_i in
-  match body with
-  | None ->
-      (match locality with
-      | Discharge ->
-          let impl = false in (* copy values from Vernacentries *)
-          let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
-	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (Discharge, VarRef id,imps)
-      | Local | Global ->
-          let k = IsAssumption Conjectural in
-          let local = match locality with
-          | Local -> true
-          | Global -> false
-          | Discharge -> assert false
-          in
-          let ctx = Univ.ContextSet.to_context ctx in
-          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
-          let kn = declare_constant id ~local decl in
-          (locality,ConstRef kn,imps))
-  | Some body ->
-      let body = norm body in
-      let k = Kindops.logical_kind_of_goal_kind kind in
-      let rec body_i t = match kind_of_term t with
-        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
-        | CoFix (0,decls) -> mkCoFix (i,decls)
-        | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
-        | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
-        | App (t, args) -> mkApp (body_i t, args)
-        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
-      let body_i = body_i body in
-      match locality with
-      | Discharge ->
-          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
-	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
-	  let c = SectionLocalDef const in
-	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Discharge,VarRef id,imps)
-      | Local | Global ->
-        let ctx = Univ.ContextSet.to_context ctx in
-        let local = match locality with
-        | Local -> true
-        | Global -> false
-        | Discharge -> assert false
-        in
-        let const =
-	  Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
-	in
-        let kn = declare_constant id ~local (DefinitionEntry const, k) in
-        (locality,ConstRef kn,imps)
-
-let save_hook = ref ignore
-let set_save_hook f = save_hook := f
-
-let save_named ?export_seff proof =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs pl do_guard persistence hook
-
-let check_anonymity id save_ident =
-  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
-    error "This command can only be used for unnamed theorem."
-
-let save_anonymous ?export_seff proof save_ident =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs pl do_guard persistence hook
-
-let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,(cstrs,pl),do_guard,_,hook = proof in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs pl do_guard
-      (Global, const.const_entry_polymorphic, Proof kind) hook
-
-(* Admitted *)
-
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
-                                spc () ++ strbrk "declared as an axiom.")
-
-let admit (id,k,e) pl hook () =
-  let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
-  let () = match k with
-  | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
-  in
-  let () = assumption_message id in
-  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
-  call_hook (fun exn -> exn) hook Global (ConstRef kn)
-
-(* Starting a goal *)
-
-let start_hook = ref ignore
-let set_start_hook = (:=) start_hook
-
-
-let get_proof proof do_guard hook opacity =
-  let (id,(const,univs,persistence)) =
-    Pfedit.cook_this_proof proof
-  in
-  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-
-let check_exist =
-  List.iter (fun (loc,id) ->
-    if not (Nametab.exists_cci (Lib.make_path id)) then
-        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
-  )
-
-let universe_proof_terminator compute_guard hook =
-  let open Proof_global in
-  make_terminator begin function
-  | Admitted (id,k,pe,(ctx,pl)) ->
-      admit (id,k,pe) pl (hook (Some ctx)) ();
-      Feedback.feedback Feedback.AddedAxiom
-  | Proved (opaque,idopt,proof) ->
-      let is_opaque, export_seff, exports = match opaque with
-        | Vernacexpr.Transparent -> false, true, []
-        | Vernacexpr.Opaque None -> true, false, []
-        | Vernacexpr.Opaque (Some l) -> true, true, l in
-      let proof = get_proof proof compute_guard
-	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
-      begin match idopt with
-      | None -> save_named ~export_seff proof
-      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
-      | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength ~export_seff proof kind id
-      end;
-      check_exist exports
-  end
-
-let standard_proof_terminator compute_guard hook =
-  universe_proof_terminator compute_guard (fun _ -> hook)
-
-let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = match terminator with
-  | None -> standard_proof_terminator compute_guard hook
-  | Some terminator -> terminator compute_guard hook
-  in
-  let sign = 
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
-  !start_hook c;
-  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-
-let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = match terminator with
-  | None -> universe_proof_terminator compute_guard hook
-  | Some terminator -> terminator compute_guard hook
-  in
-  let sign = 
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
-  !start_hook c;
-  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-
-let rec_tac_initializer finite guard thms snl =
-  if finite then
-    match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
-    | (id,_)::l -> Tactics.mutual_cofix id l 0
-    | _ -> assert false
-  else
-    (* nl is dummy: it will be recomputed at Qed-time *)
-    let nl = match snl with 
-     | None -> List.map succ (List.map List.last guard)
-     | Some nl -> nl
-    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
-       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
-       | _ -> assert false
-
-let start_proof_with_initialization kind ctx recguard thms snl hook =
-  let intro_tac (_, (_, (ids, _))) =
-    Tacticals.New.tclMAP (function
-    | Name id -> Tactics.intro_mustbe_force id
-    | Anonymous -> Tactics.intro) (List.rev ids) in
-  let init_tac,guard = match recguard with
-  | Some (finite,guard,init_tac) ->
-      let rec_tac = rec_tac_initializer finite guard thms snl in
-      Some (match init_tac with
-        | None -> 
-            if Flags.is_auto_intros () then 
-              Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
-            else
-              rec_tac
-        | Some tacl ->
-            Tacticals.New.tclTHENS rec_tac
-            (if Flags.is_auto_intros () then
-              List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
-            else
-              tacl)),guard
-  | None ->
-      let () = match thms with [_] -> () | _ -> assert false in
-      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
-  match thms with
-  | [] -> anomaly (Pp.str "No proof to start")
-  | ((id,pl),(t,(_,imps)))::other_thms ->
-      let hook ctx strength ref =
-        let ctx = match ctx with
-        | None -> Evd.empty_evar_universe_context
-        | Some ctx -> ctx
-        in
-        let other_thms_data =
-          if List.is_empty other_thms then [] else
-            (* there are several theorems defined mutually *)
-            let body,opaq = retrieve_first_recthm ref in
-            let subst = Evd.evar_universe_context_subst ctx in
-            let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = UState.context_set (*FIXME*) ctx in
-	    let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
-        let thms_data = (strength,ref,imps)::other_thms_data in
-        List.iter (fun (strength,ref,imps) ->
-	  maybe_declare_manual_implicits false ref imps;
-	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
-
-let start_proof_com ?inference_hook kind thms hook =
-  let env0 = Global.env () in
-  let levels = Option.map snd (fst (List.hd thms)) in 
-  let evdref = ref (match levels with
-		    | None -> Evd.from_env env0
-		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
-  in
-  let thms = List.map (fun (sopt,(bl,t,guard)) ->
-    let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
-    let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    let flags = all_and_fail_flags in
-    let flags = { flags with use_hook = inference_hook } in
-    evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
-    let ids = List.map get_name ctx in
-      (compute_proof_name (pi1 kind) sopt,
-      (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'),
-       guard)))
-    thms in
-  let recguard,thms,snl = look_for_possibly_mutual_statements thms in
-  let evd, nf = Evarutil.nf_evars_and_universes !evdref in
-  let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
-  let () =
-    match levels with
-    | None -> ()
-    | Some l -> ignore (Evd.universe_context evd ?names:l)
-  in
-  let evd =
-    if pi2 kind then evd
-    else (* We fix the variables to ensure they won't be lowered to Set *)
-      Evd.fix_undefined_variables evd
-  in
-    start_proof_with_initialization kind evd recguard thms snl hook
-
-
-(* Saving a proof *)
-
-let keep_admitted_vars = ref true
-
-let _ =
-  let open Goptions in
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "keep section variables in admitted proofs";
-      optkey   = ["Keep"; "Admitted"; "Variables"];
-      optread  = (fun () -> !keep_admitted_vars);
-      optwrite = (fun b -> keep_admitted_vars := b) }
-
-let save_proof ?proof = function
-  | Vernacexpr.Admitted ->
-      let pe =
-        let open Proof_global in
-        match proof with
-        | Some ({ id; entries; persistence = k; universes }, _) ->
-            if List.length entries <> 1 then
-              error "Admitted does not support multiple statements";
-            let { const_entry_secctx; const_entry_type } = List.hd entries in
-            if const_entry_type = None then
-              error "Admitted requires an explicit statement";
-            let typ = Option.get const_entry_type in
-            let ctx = Evd.evar_context_universe_context (fst universes) in
-            let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
-        | None ->
-            let pftree = Pfedit.get_pftreestate () in
-            let id, k, typ = Pfedit.current_proof_statement () in
-            let universes = Proof.initial_euctx pftree in
-            (* This will warn if the proof is complete *)
-            let pproofs, _univs =
-              Proof_global.return_proof ~allow_partial:true () in
-            let sec_vars =
-              if not !keep_admitted_vars then None
-              else match  Pfedit.get_used_variables(), pproofs with
-              | Some _ as x, _ -> x
-              | None, (pproof, _) :: _ -> 
-                  let env = Global.env () in
-                  let ids_typ = Environ.global_vars_set env typ in
-                  let ids_def = Environ.global_vars_set env pproof in
-                  Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
-              | _ -> None in
-	    let names = Pfedit.get_universe_binders () in
-            let evd = Evd.from_ctx universes in
-            let binders, ctx = Evd.universe_context ?names evd in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
-		     (universes, Some binders))
-      in
-      Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
-  | Vernacexpr.Proved (is_opaque,idopt) ->
-      let (proof_obj,terminator) =
-        match proof with
-        | None ->
-            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
-        | Some proof -> proof
-      in
-      (* if the proof is given explicitly, nothing has to be deleted *)
-      if Option.is_empty proof then Pfedit.delete_current_proof ();
-      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
-
-(* Miscellaneous *)
-
-let get_current_context () =
-  Pfedit.get_current_context ()
-           
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
deleted file mode 100644
index 39c089be..00000000
--- a/stm/lemmas.mli
+++ /dev/null
@@ -1,69 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Decl_kinds
-open Pfedit
-
-type 'a declaration_hook
-val mk_hook :
-  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
-
-val call_hook :
-  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
-
-(** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
-
-val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-   unit declaration_hook -> unit
-
-val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
-
-val start_proof_com :
-  ?inference_hook:Pretyping.inference_hook ->
-  goal_kind -> Vernacexpr.proof_expr list ->
-  unit declaration_hook -> unit
-
-val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_map ->
-  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  ((Id.t * universe_binders option) *
-     (types * (Name.t list * Impargs.manual_explicitation list))) list
-  -> int list option -> unit declaration_hook -> unit
-
-val universe_proof_terminator :
-  Proof_global.lemma_possible_guards ->
-    (Evd.evar_universe_context option -> unit declaration_hook) ->
-    Proof_global.proof_terminator
-
-val standard_proof_terminator :
-  Proof_global.lemma_possible_guards -> unit declaration_hook ->
-    Proof_global.proof_terminator
-
-(** {6 ... } *)
-
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
-
-val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-
-
-(** [get_current_context ()] returns the evar context and env of the
-   current open proof if any, otherwise returns the empty evar context
-   and the current global env *)
-
-val get_current_context : unit -> Evd.evar_map * Environ.env
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 8162fc3b..23f97612 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 open Stm
@@ -11,7 +13,7 @@ open Stm
 module Util : sig
 
 val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
 
@@ -23,8 +25,8 @@ val crawl :
 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_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
-val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
+val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
+val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
 
 end = struct
 
@@ -32,7 +34,7 @@ let unit_tag = DynBlockData.create "unit"
 let unit_val = DynBlockData.Easy.inj () unit_tag
 
 let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
-let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
+let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
 
 let simple_goal sigma g gs =
   let open Evar in
@@ -43,10 +45,10 @@ let simple_goal sigma g gs =
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
-let is_focused_goal_simple id =
-  match state_of_id id with
+let is_focused_goal_simple ~doc id =
+  match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
-  | `Valid (Some { proof }) ->
+  | `Valid (Some { Vernacstate.proof }) ->
        let proof = Proof_global.proof_of_state proof in
        let focused, r1, r2, r3, sigma = Proof.proof proof in
        let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
@@ -74,27 +76,29 @@ include Util
 (* ****************** - foo - bar - baz *********************************** *)
 
 let static_bullet ({ entry_point; prev_node } as view) =
-  match entry_point.ast with
+  assert (not (Vernacprop.has_Fail entry_point.ast));
+  match Vernacprop.under_control entry_point.ast with
   | Vernacexpr.VernacBullet b ->
       let base = entry_point.indentation in
       let last_tac = prev_node entry_point in
       crawl view ~init:last_tac (fun prev node ->
         if node.indentation < base then `Stop else
         if node.indentation > base then `Cont node else
-        match node.ast with
+        if Vernacprop.has_Fail node.ast then `Stop
+        else match Vernacprop.under_control node.ast with
         | Vernacexpr.VernacBullet b' when b = b' ->
           `Found { block_stop = entry_point.id; block_start = prev.id;
                    dynamic_switch = node.id; carry_on_data = of_bullet_val b }
         | _ -> `Stop) entry_point
   | _ -> assert false
 
-let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
-  match is_focused_goal_simple id with
+let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+         recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
       }
   | `Not -> `Leaks
 
@@ -104,9 +108,10 @@ let () = register_proof_block_delimiter
 (* ******************** { block } ***************************************** *)
   
 let static_curly_brace ({ entry_point; prev_node } as view) =
-  assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+  assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
   crawl view (fun (nesting,prev) node ->
-    match node.ast with
+    if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
+    else match Vernacprop.under_control node.ast with
     | Vernacexpr.VernacSubproof _ when nesting = 0 ->
       `Found { block_stop = entry_point.id; block_start = prev.id;
                dynamic_switch = node.id; carry_on_data = unit_val }
@@ -116,13 +121,13 @@ let static_curly_brace ({ entry_point; prev_node } as view) =
       `Cont (nesting + 1,node)
     | _ -> `Cont (nesting,node)) (-1, entry_point)
 
-let dynamic_curly_brace { dynamic_switch = id } =
-  match is_focused_goal_simple id with
+let dynamic_curly_brace doc { dynamic_switch = id } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some Vernacexpr.VernacEndSubproof
+         recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
       }
   | `Not -> `Leaks
 
@@ -138,8 +143,8 @@ let static_par { entry_point; prev_node } =
       Some { block_stop = entry_point.id; block_start = pid;
              dynamic_switch = pid; carry_on_data = unit_val }
 
-let dynamic_par { dynamic_switch = id } =
-  match is_focused_goal_simple id with
+let dynamic_par doc { dynamic_switch = id } =
+  match is_focused_goal_simple ~doc id with
   | `Simple focused ->
       `ValidBlock {
          base_state = id;
@@ -164,19 +169,19 @@ let static_indent ({ entry_point; prev_node } as view) =
         else 
           `Found { block_stop = entry_point.id; block_start = node.id;
                    dynamic_switch = node.id;
-                   carry_on_data = of_vernac_expr_val entry_point.ast }
+                   carry_on_data = of_vernac_control_val entry_point.ast }
         ) last_tac
 
-let dynamic_indent { dynamic_switch = id; carry_on_data = e } =
+let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
   Printf.eprintf "%s\n" (Stateid.to_string id);
-  match is_focused_goal_simple id with
+  match is_focused_goal_simple ~doc id with
   | `Simple [] -> `Leaks
   | `Simple focused ->
       let but_last = List.tl (List.rev focused) in 
       `ValidBlock {
          base_state = id;
          goals_to_admit = but_last;
-         recovery_command = Some (to_vernac_expr_val e);
+         recovery_command = Some (to_vernac_control_val e);
       }
   | `Not -> `Leaks
 
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index a55032a4..9784de11 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* This file implements proof block detection for:
@@ -21,7 +23,7 @@
     type).  `Simple carries the list of focused goals.
 *)
 val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
-val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
 
 type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
 
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 23538a46..4b85a05a 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -1,18 +1,16 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)
+module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index fff6d554..aa00102a 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -1,18 +1,16 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)
+module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
 
diff --git a/stm/spawned.ml b/stm/spawned.ml
index c5bd5f6f..3833c802 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 open Spawn
@@ -46,7 +48,7 @@ let control_channel = ref None
 let channels = ref None
 
 let init_channels () =
-  if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice");
+  if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice.");
   let () = match !main_channel with
   | None -> ()
   | Some (Socket(mh,mpr,mpw)) ->
@@ -65,7 +67,7 @@ let init_channels () =
   | Some (Socket (ch, cpr, cpw)) ->
     controller ch cpr cpw
   | Some AnonPipe ->
-    CErrors.anomaly (Pp.str "control channel cannot be a pipe")
+    CErrors.anomaly (Pp.str "control channel cannot be a pipe.")
 
 let get_channels () =
   match !channels with
@@ -73,3 +75,9 @@ let get_channels () =
     Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
     exit 1
   | Some(ic, oc) -> ic, oc
+
+let process_id () =
+  Printf.sprintf "%d:%s:%d" (Unix.getpid ())
+    (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+     else "master")
+    (Thread.id (Thread.self ()))
diff --git a/stm/spawned.mli b/stm/spawned.mli
index acad49f3..df4e7259 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* To link this file, threads are needed *)
@@ -20,3 +22,5 @@ val init_channels : unit -> unit
 (* Once initialized, these are the channels to talk with our master *)
 val get_channels : unit -> CThread.thread_ic * out_channel
 
+(** {6 Name of current process.} *)
+val process_id : unit -> string
diff --git a/stm/stm.ml b/stm/stm.ml
index b4331dc4..e1b90bd2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1,63 +1,113 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+(* enable in case of stm problems  *)
+(* let stm_debug () = !Flags.debug *)
+let stm_debug = ref false
 
-let prerr_endline s = if false then begin pr_err (s ()) end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (Spawned.process_id ()) s
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
 
-(* Opening ppvernac below aliases Richpp, see PR#185 *)
-let pp_to_richpp  = Richpp.richpp_of_pp
-let str_to_richpp = Richpp.richpp_of_string
+let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else ()
+let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else ()
+
+let stm_prerr_debug   s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
-open Vernacexpr
-open CErrors
 open Pp
+open CErrors
 open Names
-open Util
-open Ppvernac
-open Vernac_classifier
 open Feedback
+open Vernacexpr
 
-module Hooks = struct
+module AsyncOpts = struct
+
+  type cache = Force
+  type async_proofs = APoff | APonLazy | APon
+  type tac_error_filter = [ `None | `Only of string list | `All ]
+
+  type stm_opt = {
+    async_proofs_n_workers : int;
+    async_proofs_n_tacworkers : int;
+
+    async_proofs_cache : cache option;
+    async_proofs_mode : async_proofs;
+
+    async_proofs_private_flags : string option;
+    async_proofs_full : bool;
+    async_proofs_never_reopen_branch : bool;
+
+    async_proofs_tac_error_resilience : tac_error_filter;
+    async_proofs_cmd_error_resilience : bool;
+    async_proofs_delegation_threshold : float;
+  }
 
-let process_error, process_error_hook = Hook.make ()
-let interp, interp_hook = Hook.make ()
-let with_fail, with_fail_hook = Hook.make ()
+  let default_opts = {
+    async_proofs_n_workers = 1;
+    async_proofs_n_tacworkers = 2;
+
+    async_proofs_cache = None;
+
+    async_proofs_mode = APoff;
+
+    async_proofs_private_flags = None;
+    async_proofs_full = false;
+    async_proofs_never_reopen_branch = false;
+
+    async_proofs_tac_error_resilience = `Only [ "curly" ];
+    async_proofs_cmd_error_resilience = true;
+    async_proofs_delegation_threshold = 0.03;
+  }
+
+  let cur_opt = ref default_opts
+end
+
+open AsyncOpts
+
+let async_proofs_is_master opt =
+  opt.async_proofs_mode = APon &&
+  !Flags.async_proofs_worker_id = "master"
+
+(* Protect against state changes *)
+let stm_purify f x =
+  let st = Vernacstate.freeze_interp_state `No in
+  try
+    let res = f x in
+    Vernacstate.unfreeze_interp_state st;
+    res
+  with e ->
+    let e = CErrors.push e in
+    Vernacstate.unfreeze_interp_state st;
+    Exninfo.iraise e
+
+let execution_error ?loc state_id msg =
+    feedback ~id:state_id (Message (Error, loc, msg))
+
+module Hooks = struct
 
 let state_computed, state_computed_hook = Hook.make
  ~default:(fun state_id ~in_cache ->
-    feedback ~id:(State state_id) Processed) ()
+    feedback ~id:state_id Processed) ()
 
 let state_ready, state_ready_hook = Hook.make
  ~default:(fun state_id -> ()) ()
 
-let forward_feedback, forward_feedback_hook = 
+let forward_feedback, forward_feedback_hook =
   let m = Mutex.create () in
   Hook.make ~default:(function
-    | { id = id; route; contents } ->
-        try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
+    | { doc_id = did; span_id = id; route; contents } ->
+        try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m
         with e -> Mutex.unlock m; raise e) ()
 
-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 _ _ -> ()) ()
 
-let tactic_being_run, tactic_being_run_hook = Hook.make
- ~default:(fun _ -> ()) ()
-
 include Hook
 
 (* enables:  Hooks.(call foo args) *)
@@ -69,99 +119,37 @@ let call_process_error_once =
     match Exninfo.get info processed with
     | Some _ -> ei
     | None ->
-        let e, info = call process_error ei in
+        let e, info = ExplainErr.process_vernac_interp_error ei in
         let info = Exninfo.add info processed () in
         e, info
 
 end
 
-(* During interactive use we cache more states so that Undoing is fast *)
-let interactive () =
-  if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes
-  else `No
-
 let async_proofs_workers_extra_env = ref [||]
 
 type aast = {
   verbose : bool;
-  loc : Loc.t;
+  loc : Loc.t option;
   indentation : int;
   strlen : int;
-  mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
+  mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *)
 }
-let pr_ast { expr; indentation } = int indentation ++ str " " ++ pr_vernac expr
+let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
 
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
 
 (* Commands piercing opaque *)
 let may_pierce_opaque = function
-  | { expr = VernacPrint _ } -> true
-  | { expr = VernacExtend (("Extraction",_), _) } -> true
-  | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
-  | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
-  | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+  | VernacPrint _
+  | VernacExtend (("Extraction",_), _)
+  | VernacExtend (("SeparateExtraction",_), _)
+  | VernacExtend (("ExtractionLibrary",_), _)
+  | VernacExtend (("RecursiveExtractionLibrary",_), _)
+  | VernacExtend (("ExtractionConstant",_), _)
+  | VernacExtend (("ExtractionInlinedConstant",_), _)
+  | VernacExtend (("ExtractionInductive",_), _) -> true
   | _ -> 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
-    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;
-    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
-    try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
-    with e ->
-      let e = CErrors.push e in
-      iraise Hooks.(call_process_error_once e)
-  end
-
-(* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let indentation_of_string s =
-  let len = String.length s in
-  let rec aux n i precise =
-    if i >= len then 0, precise, len
-    else
-      match s.[i] with
-      | ' ' | '\t' -> aux (succ n) (succ i) precise
-      | '\n' | '\r' -> aux 0 (succ i) true
-      | _ -> n, precise, len in
-  aux 0 0 false
-
-let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
-  let feedback_id = 
-    if Option.is_empty newtip then Edit eid
-    else State (Option.get newtip) in
-  let indentation, precise, strlen = indentation_of_string s in
-  let indentation =
-    if precise then indentation else indlen_prev () + indentation in
-  set_id_for_feedback ?route feedback_id;
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  Flags.with_option Flags.we_are_parsing (fun () ->
-    try
-      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
-      | None -> raise (Invalid_argument "vernac_parse")
-      | Some (loc, ast) -> indentation, strlen, loc, ast
-    with e when CErrors.noncritical e ->
-      let (e, info) = CErrors.push e in
-      let loc = Option.default Loc.ghost (Loc.get_loc info) in
-      Hooks.(call parse_error feedback_id loc (iprint (e, info)));
-      iraise (e, info))
-  ()
-
-let pr_open_cur_subgoals () =
-  try Printer.pr_open_subgoals ()
-  with Proof_global.NoCurrentProof -> Pp.str ""
-
 let update_global_env () =
   if Proof_global.there_are_pending_proofs () then
     Proof_global.update_global_env ()
@@ -170,7 +158,6 @@ module Vcs_ = Vcs.Make(Stateid.Self)
 type future_proof = Proof_global.closed_proof_output Future.computation
 type proof_mode = string
 type depth = int
-type cancel_switch = bool ref
 type branch_type =
   [ `Master
   | `Proof of proof_mode * depth
@@ -181,22 +168,23 @@ type cmd_t = {
   ctac : bool; (* is a tactic *)
   ceff : bool; (* is a side-effecting command in the middle of a proof *)
   cast : aast;
-  cids : Id.t list;
+  cids : Names.Id.t list;
   cblock : proof_block_name option;
   cqueue : [ `MainQueue
-           | `TacQueue of solving_tac * anon_abstracting_tac * cancel_switch
-           | `QueryQueue of cancel_switch
+           | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch
+           | `QueryQueue of AsyncTaskQueue.cancel_switch
            | `SkipQueue ] }
-type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Names.Id.t list
 type qed_t = {
   qast : aast;
   keep : vernac_qed_type;
-  mutable fproof : (future_proof * cancel_switch) option;
+  mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option;
   brname : Vcs_.Branch.t;
   brinfo : branch_type Vcs_.branch_info
 }
-type seff_t = aast option
+type seff_t = ReplayCommand of aast | CherryPickEnv
 type alias_t = Stateid.t * aast
+
 type transaction =
   | Cmd    of cmd_t
   | Fork   of fork_t
@@ -208,30 +196,30 @@ type step =
   [ `Cmd    of cmd_t
   | `Fork   of fork_t * Stateid.t option
   | `Qed    of qed_t * Stateid.t
-  | `Sideff of [ `Ast of aast * Stateid.t | `Id of Stateid.t ]
+  | `Sideff of seff_t * Stateid.t
   | `Alias  of alias_t ]
+
 type visit = { step : step; next : Stateid.t }
 
 let mkTransTac cast cblock cqueue =
   Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false }
+
 let mkTransCmd cast cids ceff cqueue =
   Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
 
 (* Parts of the system state that are morally part of the proof state *)
-let summary_pstate = [ Evarutil.meta_counter_summary_name;
-                       Evd.evar_counter_summary_name;
-                       "program-tcc-table" ]
+let summary_pstate = Evarutil.meta_counter_summary_tag,
+                     Evd.evar_counter_summary_tag,
+                     Obligations.program_tcc_summary_tag
+
 type cached_state =
   | Empty
   | Error of Exninfo.iexn
-  | Valid of state
-and state = { (* TODO: inline records in OCaml 4.03 *)
-  system : States.state;       (* summary + libstack *)
-  proof : Proof_global.state;  (* proof state *)
-  shallow : bool               (* is the state trimmed down (libstack) *)
-}
+  | Valid of Vernacstate.t
+
 type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
 type backup = { mine : branch; others : branch list }
+
 type 'vcs state_info = { (* TODO: Make this record private to VCS *)
   mutable n_reached : int;      (* debug cache: how many times was computed *)
   mutable n_goals : int;        (* open goals: indentation *)
@@ -241,7 +229,7 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
 let default_info () =
   { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
 
-module DynBlockData : Dyn.S = Dyn.Make(struct end)
+module DynBlockData : Dyn.S = Dyn.Make ()
 
 (* Clusters of nodes implemented as Dag properties.  While Dag and Vcs impose
  * no constraint on properties, here we impose boxes to be non overlapping.
@@ -276,7 +264,7 @@ end = struct (* {{{ *)
 
   let proof_nesting vcs =
     List.fold_left max 0
-      (List.map_filter
+      (CList.map_filter
         (function
          | { Vcs_.kind = `Proof (_,n) } -> Some n
          | { Vcs_.kind = `Edit _ } -> Some 1
@@ -286,7 +274,7 @@ end = struct (* {{{ *)
   let find_proof_at_depth vcs pl =
     try List.find (function
           | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
-          | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
+          | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.")
           | _ -> false)
         (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
     with Not_found -> failwith "find_proof_at_depth"
@@ -294,9 +282,9 @@ end = struct (* {{{ *)
   exception Expired
   let visit vcs id =
     if Stateid.equal id Stateid.initial then
-      anomaly(Pp.str "Visiting the initial state id")
+      anomaly(Pp.str "Visiting the initial state id.")
     else if Stateid.equal id Stateid.dummy then
-      anomaly(Pp.str "Visiting the dummy state id")
+      anomaly(Pp.str "Visiting the dummy state id.")
     else
     try
       match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -307,12 +295,12 @@ end = struct (* {{{ *)
       | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n }
       | [n, Qed x; p, Noop]
       | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n }
-      | [n, Sideff None; p, Noop]
-      | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n }
-      | [n, Sideff (Some x); p, Noop]
-      | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
-      | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
-      | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
+      | [n, Sideff CherryPickEnv; p, Noop]
+      | [p, Noop; n, Sideff CherryPickEnv]-> { step = `Sideff (CherryPickEnv, p); next = n }
+      | [n, Sideff (ReplayCommand x); p, Noop]
+      | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n }
+      | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n}
+      | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id^"."))
     with Not_found -> raise Expired
 
 end (* }}} *)
@@ -320,6 +308,16 @@ end (* }}} *)
 (*************************** THE DOCUMENT *************************************)
 (******************************************************************************)
 
+(* The main document type associated to a VCS *)
+type stm_doc_type =
+  | VoDoc       of string
+  | VioDoc      of string
+  | Interactive of Names.DirPath.t
+
+(* Dummy until we land the functional interp patch + fixed start_library *)
+type doc = int
+let dummy_doc : doc = 0
+
 (* Imperative wrap around VCS to obtain _the_ VCS that is the
  * representation of the document Coq is currently processing *)
 module VCS : sig
@@ -336,7 +334,13 @@ module VCS : sig
 
   type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
 
-  val init : id -> unit
+  val init : stm_doc_type -> id -> doc
+  (* val get_type : unit -> stm_doc_type *)
+  val set_ldir : Names.DirPath.t -> unit
+  val get_ldir : unit -> Names.DirPath.t
+
+  val is_interactive : unit -> [`Yes | `No | `Shallow]
+  val is_vio_doc : unit -> bool
 
   val current_branch : unit -> Branch.t
   val checkout : Branch.t -> unit
@@ -364,7 +368,7 @@ module VCS : sig
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : block_start:id -> block_stop:id -> vcs
   val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list
-  
+
   val create_proof_task_box : id list -> qed:id -> block_start:id -> unit
   val create_proof_block : static_block_declaration -> string -> unit
   val box_of : id -> box list
@@ -373,7 +377,7 @@ module VCS : sig
 
   val proof_nesting : unit -> int
   val checkout_shallowest_proof_branch : unit -> unit
-  val propagate_sideff : replay:aast option -> unit
+  val propagate_sideff : action:seff_t -> unit
 
   val gc : unit -> unit
 
@@ -392,19 +396,28 @@ end = struct (* {{{ *)
   open Printf
 
   let print_dag vcs () =
+
+    (* Due to threading, be wary that this will be called from the
+       toplevel with we_are_parsing set to true, as indeed, the
+       toplevel is waiting for input . What a race! XD
+
+       In case you are hitting the race enable stm_debug.
+    *)
+    if !stm_debug then Flags.we_are_parsing := false;
+
     let fname =
-      "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
+      "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in
     let string_of_transaction = function
       | Cmd { cast = t } | Fork (t, _,_,_) ->
           (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
-      | Sideff (Some t) ->
+      | Sideff (ReplayCommand t) ->
           sprintf "Sideff(%s)"
             (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
-      | Sideff None -> "EnvChange"
+      | Sideff CherryPickEnv -> "EnvChange"
       | Noop -> " "
       | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
-      | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
-    let is_green id = 
+      | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
+    let is_green id =
       match get_info vcs id with
       | Some { state = Valid _ } -> true
       | _ -> false in
@@ -472,7 +485,7 @@ end = struct (* {{{ *)
     let outerboxes boxes =
        List.filter (fun b ->
          not (List.exists (fun b1 ->
-           not (same_box b1 b) && contains b1 b) boxes)           
+           not (same_box b1 b) && contains b1 b) boxes)
          ) boxes in
     let rec rec_print b =
       boxes := CList.remove same_box b !boxes;
@@ -509,9 +522,30 @@ end = struct (* {{{ *)
   type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
-  let init id =
+  let doc_type = ref (Interactive (Names.DirPath.make []))
+  let ldir = ref Names.DirPath.empty
+
+  let init dt id =
+    doc_type := dt;
     vcs := empty id;
-    vcs := set_info !vcs id (default_info ())
+    vcs := set_info !vcs id (default_info ());
+    dummy_doc
+
+  let set_ldir ld =
+    ldir := ld
+
+  let get_ldir () = !ldir
+  (* let get_type () = !doc_type *)
+
+  let is_interactive () =
+    match !doc_type with
+    | Interactive _ -> `Yes
+    | _ -> `No
+
+  let is_vio_doc () =
+    match !doc_type with
+    | VioDoc _ -> true
+    | _ -> false
 
   let current_branch () = current_branch !vcs
 
@@ -532,9 +566,9 @@ end = struct (* {{{ *)
     vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
-    (match x with
-    | VernacDefinition (_,((_,i),_),_) -> string_of_id i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
+    (match Vernacprop.under_control x with
+    | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
+    | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -544,7 +578,7 @@ end = struct (* {{{ *)
     | None -> raise Vcs_aux.Expired
   let set_state id s =
     (get_info id).state <- s;
-    if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
+    if async_proofs_is_master !cur_opt then Hooks.(call state_ready id)
   let get_state id = (get_info id).state
   let reached id =
     let info = get_info id in
@@ -558,7 +592,7 @@ end = struct (* {{{ *)
     if List.mem edit_branch (Vcs_.branches !vcs) then begin
       checkout edit_branch;
       match get_branch edit_branch with
-      | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
+      | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
       | _ -> assert false
     end else
       let pl = proof_nesting () in
@@ -566,20 +600,20 @@ end = struct (* {{{ *)
         let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
-        prerr_endline (fun () -> "mode:" ^ mode);
-        Proof_global.activate_proof_mode mode
+        stm_prerr_endline (fun () -> "mode:" ^ mode);
+        Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
       with Failure _ ->
         checkout Branch.master;
-        Proof_global.disactivate_current_proof_mode ()
+        Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
 
   (* copies the transaction on every open branch *)
-  let propagate_sideff ~replay:t =
+  let propagate_sideff ~action =
     List.iter (fun b ->
       checkout b;
       let id = new_node () in
-      merge id ~ours:(Sideff t) ~into:b Branch.master)
+      merge id ~ours:(Sideff action) ~into:b Branch.master)
     (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
-  
+
   let visit id = Vcs_aux.visit !vcs id
 
   let nodes_in_slice ~block_start ~block_stop =
@@ -588,10 +622,10 @@ end = struct (* {{{ *)
       match visit id with
       | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
       | { next = n; step = `Alias x } -> (id,Alias x) :: aux n
-      | { next = n; step = `Sideff (`Ast (x,_)) } ->
-           (id,Sideff (Some x)) :: aux n
-      | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^
-                         " to "^Stateid.to_string block_stop))
+      | { next = n; step = `Sideff (ReplayCommand x,_) } ->
+           (id,Sideff (ReplayCommand x)) :: aux n
+      | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^
+                         " to "^Stateid.to_string block_stop^"."))
     in aux block_stop
 
   let slice ~block_start ~block_stop =
@@ -643,11 +677,11 @@ end = struct (* {{{ *)
       l
 
   let create_proof_task_box l ~qed ~block_start:lemma =
-    if not (topo_invariant l) then anomaly (str "overlapping boxes");
+    if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
     vcs := create_property !vcs l (ProofTask { qed; lemma })
   let create_proof_block ({ block_start; block_stop} as decl) name =
     let l = nodes_in_slice ~block_start ~block_stop in
-    if not (topo_invariant l) then anomaly (str "overlapping boxes");
+    if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
     vcs := create_property !vcs l (ProofBlock (decl, name))
   let box_of id = List.map Dag.Property.data (property_of !vcs id)
   let delete_boxes_of id =
@@ -658,7 +692,7 @@ end = struct (* {{{ *)
     with
     | [] -> None
     | [x] -> Some x
-    | _ -> anomaly (str "node with more than 1 proof task box")
+    | _ -> anomaly Pp.(str "node with more than 1 proof task box.")
 
   let gc () =
     let old_vcs = !vcs in
@@ -678,7 +712,7 @@ end = struct (* {{{ *)
     val command : now:bool -> (unit -> unit) -> unit
 
   end = struct
-    
+
     let m = Mutex.create ()
     let c = Condition.create ()
     let job = ref None
@@ -719,7 +753,7 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
-let state_of_id id =
+let state_of_id ~doc id =
   try match (VCS.get_info id).state with
     | Valid s -> `Valid (Some s)
     | Error (e,_) -> `Error e
@@ -729,7 +763,7 @@ let state_of_id id =
 
 (****** A cache: fills in the nodes of the VCS document with their value ******)
 module State : sig
-  
+
   (** The function is from unit, so it uses the current state to define
       a new one.  I.e. one may been to install the right state before
       defining a new one.
@@ -739,26 +773,36 @@ module State : sig
     ?safe_id:Stateid.t ->
     ?redefine:bool -> ?cache:Summary.marshallable ->
     ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
-  val fix_exn_ref : (iexn -> iexn) ref
+
+  val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
 
   val install_cached : Stateid.t -> unit
   val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
   val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
 
+  val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
 
-  val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn
   (* to send states across worker/master *)
-  type frozen_state
-  val get_cached : Stateid.t -> frozen_state
-  val same_env : frozen_state -> frozen_state -> bool
+  val get_cached : Stateid.t -> Vernacstate.t
+  val same_env : Vernacstate.t -> Vernacstate.t -> bool
 
   type proof_part
+
   type partial_state =
-    [ `Full of frozen_state
-    | `Proof of Stateid.t * proof_part ]
-  val proof_part_of_frozen : frozen_state -> proof_part
+    [ `Full of Vernacstate.t
+    | `ProofOnly of Stateid.t * proof_part ]
+
+  val proof_part_of_frozen : Vernacstate.t -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
+  (* Handlers for initial state, prior to document creation. *)
+  val register_root_state : unit -> unit
+  val restore_root_state : unit -> unit
+
+  (* Only for internal use to catch problems in parse_sentence, should
+     be removed in the state handling refactoring.  *)
+  val cur_id : Stateid.t ref
+
 end = struct (* {{{ *)
 
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
@@ -766,31 +810,26 @@ end = struct (* {{{ *)
   let cur_id = ref Stateid.dummy
   let fix_exn_ref = ref (fun x -> x)
 
-  (* helpers *)
-  let freeze_global_state marshallable =
-    { system = States.freeze ~marshallable;
-      proof = Proof_global.freeze ~marshallable;
-      shallow = (marshallable = `Shallow) }
-  let unfreeze_global_state { system; proof } =
-    States.unfreeze system; Proof_global.unfreeze proof
-
-  (* hack to make futures functional *)
-  let () = Future.set_freeze
-    (fun () -> Obj.magic (freeze_global_state `No, !cur_id))
-    (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i)
-  
-  type frozen_state = state
   type proof_part =
-    Proof_global.state * Summary.frozen_bits (* only meta counters *)
+    Proof_global.t *
+    int *                                   (* Evarutil.meta_counter_summary_tag *)
+    int *                                   (* Evd.evar_counter_summary_tag *)
+    Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+
   type partial_state =
-    [ `Full of frozen_state
-    | `Proof of Stateid.t * proof_part ]
-  let proof_part_of_frozen { proof; system } =
+    [ `Full of Vernacstate.t
+    | `ProofOnly of Stateid.t * proof_part ]
+
+  let proof_part_of_frozen { Vernacstate.proof; system } =
+    let st = States.summary_of_state system in
     proof,
-    Summary.project_summary (States.summary_of_state system) summary_pstate
+    Summary.project_from_summary st Util.(pi1 summary_pstate),
+    Summary.project_from_summary st Util.(pi2 summary_pstate),
+    Summary.project_from_summary st Util.(pi3 summary_pstate)
 
   let freeze marshallable id =
-    VCS.set_state id (Valid (freeze_global_state marshallable))
+    VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable))
+
   let freeze_invalid id iexn = VCS.set_state id (Error iexn)
 
   let is_cached ?(cache=`No) id only_valid =
@@ -813,21 +852,26 @@ end = struct (* {{{ *)
   let install_cached id =
     match VCS.get_info id with
     | { state = Valid s } ->
-         if Stateid.equal id !cur_id then () (* optimization *)
-         else begin unfreeze_global_state s; cur_id := id end
-    | { state = Error ie } -> cur_id := id; Exninfo.iraise ie 
+       Vernacstate.unfreeze_interp_state s;
+       cur_id := id
+
+    | { state = Error ie } ->
+       cur_id := id;
+       Exninfo.iraise ie
+
     | _ ->
         (* coqc has a 1 slot cache and only for valid states *)
-        if interactive () = `No && Stateid.equal id !cur_id then ()
-        else anomaly (str "installing a non cached state")
+        if VCS.is_interactive () = `No && Stateid.equal id !cur_id then ()
+        else anomaly Pp.(str "installing a non cached state.")
 
   let get_cached id =
     try match VCS.get_info id with
     | { state = Valid s } -> s
-    | _ -> anomaly (str "not a cached state")
-    with VCS.Expired -> anomaly (str "not a cached state (expired)")
+    | _ -> anomaly Pp.(str "not a cached state.")
+    with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
 
   let assign id what =
+    let open Vernacstate in
     if VCS.get_state id <> Empty then () else
     try match what with
     | `Full s ->
@@ -835,22 +879,27 @@ end = struct (* {{{ *)
            try
             let prev = (VCS.visit id).next in
             if is_cached_and_valid prev
-            then { s with proof = 
+            then { s with proof =
               Proof_global.copy_terminators
                 ~src:(get_cached prev).proof ~tgt:s.proof }
             else s
            with VCS.Expired -> s in
          VCS.set_state id (Valid s)
-    | `Proof(ontop,(pstate,counters)) ->
+    | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
            let s = { s with proof =
              Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
-               (Summary.surgery_summary
-                 (States.summary_of_state s.system)
-               counters) } in
+               begin
+                 let st = States.summary_of_state s.system in
+                 let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in
+                 let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in
+                 let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in
+                 st
+               end
+                } in
            VCS.set_state id (Valid s)
     with VCS.Expired -> ()
 
@@ -858,27 +907,27 @@ end = struct (* {{{ *)
     match Stateid.get info with
     | Some _ -> (e, info)
     | None ->
-        let loc = Option.default Loc.ghost (Loc.get_loc info) in
+        let loc = 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 ?loc id (iprint (e, info));
         (e, Stateid.add info ~valid id)
 
-  let same_env { system = s1 } { system = s2 } =
+  let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
     let s1 = States.summary_of_state s1 in
-    let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in
+    let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in
     let s2 = States.summary_of_state s2 in
-    let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in
-    Summary.pointer_equal e1 e2
+    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)
         f id
   =
-    feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
+    feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
     let str_id = Stateid.to_string id in
     if is_cached id && not redefine then
-      anomaly (str"defining state "++str str_id++str" twice");
+      anomaly Pp.(str"defining state "++str str_id++str" twice.");
     try
-      prerr_endline (fun () -> "defining "^str_id^" (cache="^
+      stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
@@ -886,7 +935,7 @@ end = struct (* {{{ *)
       fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
-      prerr_endline (fun () -> "setting cur id to "^str_id);
+      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);
@@ -908,8 +957,138 @@ end = struct (* {{{ *)
       Hooks.(call unreachable_state id ie);
       Exninfo.iraise ie
 
+  let init_state = ref None
+
+  let register_root_state () =
+    init_state := Some (Vernacstate.freeze_interp_state `No)
+
+  let restore_root_state () =
+    cur_id := Stateid.dummy;
+    Vernacstate.unfreeze_interp_state (Option.get !init_state);
+
 end (* }}} *)
 
+(* indentation code for Show Script, initially contributed
+ * by D. de Rauglaudre. Should be moved away.
+ *)
+
+module ShowScript = struct
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+  (* ng1 : number of goals remaining at the current level (before cmd)
+     ngl1 : stack of previous levels with their remaining goals
+     ng : number of goals after the execution of cmd
+     beginend : special indentation stack for { } *)
+  let ngprev = List.fold_left (+) ng1 ngl1 in
+  let new_ngl =
+    if ng > ngprev then
+      (* We've branched *)
+      (ng - ngprev + 1, ng1 - 1 :: ngl1)
+    else if ng < ngprev then
+      (* A subgoal have been solved. Let's compute the new current level
+	 by discarding all levels with 0 remaining goals. *)
+      let rec loop = function
+	| (0, ng2::ngl2) -> loop (ng2,ngl2)
+	| p -> p
+      in loop (ng1-1, ngl1)
+    else
+      (* Standard case, same goal number as before *)
+      (ng1, ngl1)
+  in
+  (* When a subgoal have been solved, separate this block by an empty line *)
+  let new_nl = (ng < ngprev)
+  in
+  (* Indentation depth *)
+  let ind = List.length ngl1
+  in
+  (* Some special handling of bullets and { }, to get a nicer display *)
+  let pred n = max 0 (n-1) in
+  let ind, nl, new_beginend = match Vernacprop.under_control cmd with
+    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+    | VernacBullet _ -> pred ind, nl, beginend
+    | _ -> ind, nl, beginend
+  in
+  let pp = Pp.(
+    (if nl then fnl () else mt ()) ++
+    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)))
+  in
+  (new_ngl, new_nl, new_beginend, pp :: ppl)
+
+let get_script prf =
+  let branch, test =
+    match prf with
+    | None -> VCS.Branch.master, fun _ -> true
+    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
+  let rec find acc id =
+    if Stateid.equal id Stateid.initial ||
+       Stateid.equal id Stateid.dummy then acc else
+    let view = VCS.visit id in
+    match view.step with
+    | `Fork((_,_,_,ns), _) when test ns -> acc
+    | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
+    | `Sideff (ReplayCommand x,_) ->
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+    | `Sideff (CherryPickEnv, id)  -> find acc id
+    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+    | `Cmd _ -> find acc view.next
+    | `Alias (id,_) -> find acc id
+    | `Fork _ -> find acc view.next
+    in
+  find [] (VCS.get_branch_pos branch)
+
+let show_script ?proof () =
+  try
+    let prf =
+      try match proof with
+      | None -> Some (Proof_global.get_current_proof_name ())
+      | Some (p,_) -> Some (p.Proof_global.id)
+      with Proof_global.NoCurrentProof -> None
+    in
+    let cmds = get_script prf in
+    let _,_,_,indented_cmds =
+      List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+    in
+    let indented_cmds = List.rev (indented_cmds) in
+    msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+  with Vcs_aux.Expired -> ()
+
+end
+
+(* Wrapper for Vernacentries.interp to set the feedback id *)
+(* It is currently called 19 times, this number should be certainly
+   reduced... *)
+let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t =
+  (* The Stm will gain the capability to interpret commmads affecting
+     the whole document state, such as backtrack, etc... so we start
+     to design the stm command interpreter now *)
+  set_id_for_feedback ?route dummy_doc 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 is_filtered_command = function
+    | VernacResetName _ | VernacResetInitial | VernacBack _
+    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+    | _ -> false
+  in
+  let aux_interp st expr =
+    let cmd = Vernacprop.under_control expr in
+    if is_filtered_command cmd then
+      (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
+    else
+      match cmd with
+      | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *)
+      | _ ->
+        stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
+        with e ->
+          let e = CErrors.push e in
+          Exninfo.iraise Hooks.(call_process_error_once e)
+  in aux_interp st expr
 
 (****************************** CRUFT *****************************************)
 (******************************************************************************)
@@ -919,13 +1098,12 @@ module Backtrack : sig
 
   val record : unit -> unit
   val backto : Stateid.t -> unit
-  val back_safe : unit -> unit
 
   (* we could navigate the dag, but this ways easy *)
   val branches_of : Stateid.t -> backup
 
-  (* To be installed during initialization *)
-  val undo_vernac_classifier : vernac_expr -> vernac_classification
+  (* Returns the state that the command should backtract to *)
+  val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when
 
 end = struct (* {{{ *)
 
@@ -948,16 +1126,16 @@ end = struct (* {{{ *)
     let info = VCS.get_info oid in
     match info.vcs_backup with
     | None, _ ->
-       anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
-               str": a state with no vcs_backup")
+       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
     | _, None ->
-       anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
-               str": a state with no vcs_backup")
+       anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++
+                   str": a state with no vcs_backup.")
     | _, Some x -> x
 
   let rec fold_until f acc id =
@@ -973,52 +1151,59 @@ end = struct (* {{{ *)
           match VCS.visit id with
           | { step = `Fork ((_,_,_,l),_) } -> l, false,0
           | { step = `Cmd { cids = l; ctac } } -> l, ctac,0
-          | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n
+          | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
+          begin match Vernacprop.under_control expr with
+                | VernacUndo n -> [], false, n
+                | _ -> [],false,0
+          end
           | _ -> [],false,0 in
         match f acc (id, vcs, ids, tactic, undo) with
         | `Stop x -> x
         | `Cont acc -> next acc
- 
-  let back_safe () =
-    let id =
-      fold_until (fun n (id,_,_,_,_) ->
-        if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n))
-        0 (VCS.get_branch_pos (VCS.current_branch ())) in
-    backto id
+
+  let undo_costly_in_batch_mode =
+    CWarnings.create ~name:"undo-batch-mode" ~category:"non-interactive" Pp.(fun v ->
+        str "Command " ++ Ppvernac.pr_vernac v ++
+        str (" is not recommended in batch mode. In particular, going back in the document" ^
+             " is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^
+             " 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 =
+    if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
+    then undo_costly_in_batch_mode v;
     try
-      match v with
+      match Vernacprop.under_control v with
       | VernacResetInitial ->
-          VtStm (VtBack Stateid.initial, true), VtNow
-      | VernacResetName (_,name) ->
+          Stateid.initial, VtNow
+      | VernacResetName {CAst.v=name} ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
             let oid =
               fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
-            VtStm (VtBack oid, true), VtNow
+            oid, VtNow
           with Not_found ->
-            VtStm (VtBack id, true), VtNow)
+            id, VtNow)
       | VernacBack n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          VtStm (VtBack oid, true), VtNow
+          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
-          VtStm (VtBack oid, true), VtLater
+          oid, VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let vcs =
-            match (VCS.get_info id).vcs_backup with 
-            | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
+            match (VCS.get_info id).vcs_backup with
+            | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.")
             | Some vcs, _ -> vcs in
           let cb, _ =
             try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
@@ -1028,53 +1213,50 @@ end = struct (* {{{ *)
             0 id in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
-          VtStm (VtBack oid, true), VtLater
+          oid, VtLater
       | VernacAbortAll ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
-          VtStm (VtBack oid, true), VtLater
+          oid, VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
-      | _ -> VtUnknown, VtNow
+          Stateid.of_int id, VtNow
+      | _ -> anomaly Pp.(str "incorrect VtMeta classification")
     with
     | Not_found ->
-       CErrors.errorlabstrm "undo_vernac_classifier"
-        (str "Cannot undo")
+       CErrors.user_err ~hdr:"undo_vernac_classifier"
+        Pp.(str "Cannot undo")
 
 end (* }}} *)
 
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
+
 let get_hint_ctx loc =
-  let s = Aux_file.get !hints loc "context_used" in
-  match Str.split (Str.regexp ";") s with
-  | ids :: _ ->
-      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
-      let ids = List.map (fun id -> Loc.ghost, id) ids in
-      begin match ids with
-      | [] -> SsEmpty
-      | x :: xs ->
-          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
-      end
-  | _ -> raise Not_found
+  let s = Aux_file.get ?loc !hints "context_used" in
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> CAst.make id) ids in
+  match ids with
+  | [] -> SsEmpty
+  | x :: xs ->
+    List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
 
 let get_hint_bp_time proof_name =
-  try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
+  try float_of_string (Aux_file.get !hints proof_name)
   with Not_found -> 1.0
 
-let record_pb_time proof_name loc time =
+let record_pb_time ?loc proof_name time =
   let proof_build_time = Printf.sprintf "%.3f" time in
-  Aux_file.record_in_aux_at loc "proof_build_time" proof_build_time;
+  Aux_file.record_in_aux_at ?loc "proof_build_time" proof_build_time;
   if proof_name <> "" then begin
-    Aux_file.record_in_aux_at Loc.ghost proof_name proof_build_time;
-    hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
+    Aux_file.record_in_aux_at proof_name proof_build_time;
+    hints := Aux_file.set !hints proof_name proof_build_time
   end
- 
-exception RemoteException of std_ppcmds
+
+exception RemoteException of Pp.t
 let _ = CErrors.register_handler (function
   | RemoteException ppcmd -> ppcmd
   | _ -> raise Unhandled)
@@ -1084,7 +1266,7 @@ let _ = CErrors.register_handler (function
 
 type document_node = {
   indentation : int;
-  ast : Vernacexpr.vernac_expr;
+  ast : Vernacexpr.vernac_control;
   id : Stateid.t;
 }
 
@@ -1099,23 +1281,23 @@ type static_block_detection =
 type recovery_action = {
   base_state : Stateid.t;
   goals_to_admit : Goal.goal list;
-  recovery_command : Vernacexpr.vernac_expr option;
+  recovery_command : Vernacexpr.vernac_control option;
 }
 
 type dynamic_block_error_recovery =
-  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+  doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
 
 let proof_block_delimiters = ref []
 
 let register_proof_block_delimiter name static dynamic =
   if List.mem_assoc name !proof_block_delimiters then
-    CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+    CErrors.user_err ~hdr:"STM" Pp.(str "Duplicate block delimiter " ++ str name);
   proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
 
 let mk_doc_node id = function
   | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
        Some { indentation; ast = expr; id }
-  | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } ->
+  | { step = `Sideff (ReplayCommand { indentation; expr }, _); next } ->
        Some { indentation; ast = expr; id }
   | _ -> None
 let prev_node { id } =
@@ -1124,15 +1306,15 @@ let prev_node { id } =
 let cur_node id = mk_doc_node id (VCS.visit id)
 
 let is_block_name_enabled name =
-  match !Flags.async_proofs_tac_error_resilience with
+  match !cur_opt.async_proofs_tac_error_resilience with
   | `None -> false
   | `All -> true
   | `Only l -> List.mem name l
 
 let detect_proof_block id name =
-  let name = match name with None -> "indent" | Some x -> x in   
+  let name = match name with None -> "indent" | Some x -> x in
   if is_block_name_enabled name &&
-     (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ())
+     (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ())
   then (
   match cur_node id with
   | None -> ()
@@ -1144,14 +1326,16 @@ let detect_proof_block id name =
           VCS.create_proof_block decl name
       end
     with Not_found ->
-      CErrors.errorlabstrm "STM"
-        (str "Unknown proof block delimiter " ++ str name)
+      CErrors.user_err ~hdr:"STM"
+        Pp.(str "Unknown proof block delimiter " ++ str name)
   )
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
 
+(* Unused module warning doesn't understand [module rec] *)
+[@@@ocaml.warning "-60"]
 module rec ProofTask : sig
- 
+
   type competence = Stateid.t list
   type task_build_proof = {
     t_exn_info : Stateid.t * Stateid.t;
@@ -1160,7 +1344,7 @@ module rec ProofTask : sig
     t_drop     : bool;
     t_states   : competence;
     t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
-    t_loc      : Loc.t;
+    t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
 
@@ -1174,16 +1358,17 @@ module rec ProofTask : sig
 
   include AsyncTaskQueue.Task
   with type task := task
-  and  type competence := competence
-  and  type request := request
+   and type competence := competence
+   and type request := request
 
   val build_proof_here :
+    ?loc:Loc.t ->
     drop_pt:bool ->
-    Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
+    Stateid.t * Stateid.t -> Stateid.t ->
       Proof_global.closed_proof_output Future.computation
 
   (* If set, only tasks overlapping with this list are processed *)
-  val set_perspective : Stateid.t list -> unit  
+  val set_perspective : Stateid.t list -> unit
 
 end = struct (* {{{ *)
 
@@ -1197,7 +1382,7 @@ end = struct (* {{{ *)
     t_drop     : bool;
     t_states   : competence;
     t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
-    t_loc      : Loc.t;
+    t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
 
@@ -1205,21 +1390,22 @@ end = struct (* {{{ *)
     | BuildProof of task_build_proof
     | States of Stateid.t list
 
+  type worker_status = Fresh | Old of competence
+
   type request =
   | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence
   | ReqStates of Stateid.t list
-  
+
   type error = {
     e_error_at    : Stateid.t;
     e_safe_id     : Stateid.t;
-    e_msg         : std_ppcmds;
+    e_msg         : Pp.t;
     e_safe_states : Stateid.t list }
 
   type response =
     | RespBuiltProof of Proof_global.closed_proof_output * float
     | RespError of error
     | RespStates of (Stateid.t * State.partial_state) list
-    | RespDone
 
   let name = ref "proofworker"
   let extra_env () = !async_proofs_workers_extra_env
@@ -1229,10 +1415,10 @@ end = struct (* {{{ *)
 
   let task_match age t =
     match age, t with
-    | `Fresh, BuildProof { t_states } ->
-        not !Flags.async_proofs_full ||
+    | Fresh, BuildProof { t_states } ->
+        not !cur_opt.async_proofs_full ||
         List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states
-    | `Old my_states, States l ->
+    | Old my_states, States l ->
         List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
     | _ -> false
 
@@ -1248,7 +1434,7 @@ end = struct (* {{{ *)
     | BuildProof {
         t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states;t_drop
       } ->
-        assert(age = `Fresh);
+        assert(age = Fresh);
         try Some (ReqBuildProof ({
           Stateid.exn_info = t_exn_info;
           stop = t_stop;
@@ -1258,19 +1444,19 @@ end = struct (* {{{ *)
           name = t_name }, t_drop, t_states))
         with VCS.Expired -> None
 
-  let use_response (s : competence AsyncTaskQueue.worker_status) t r =
+  let use_response (s : worker_status) t r =
     match s, t, r with
-    | `Old c, States _, RespStates l ->
+    | Old c, States _, RespStates l ->
         List.iter (fun (id,s) -> State.assign id s) l; `End
-    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
+    | Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
               RespBuiltProof (pl, time) ->
         feedback (InProgress ~-1);
         t_assign (`Val pl);
-        record_pb_time t_name t_loc time;
-        if !Flags.async_proofs_full || t_drop
+        record_pb_time ?loc:t_loc t_name time;
+        if !cur_opt.async_proofs_full || t_drop
         then `Stay(t_states,[States t_states])
         else `End
-    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
+    | Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
         feedback (InProgress ~-1);
         let info = Stateid.add ~valid Exninfo.null e_error_at in
@@ -1285,21 +1471,21 @@ end = struct (* {{{ *)
     | Some (BuildProof { t_start = start; t_assign }) ->
         let s = "Worker dies or task expired" in
         let info = Stateid.add ~valid:start Exninfo.null start in
-        let e = (RemoteException (strbrk s), info) in
+        let e = (RemoteException (Pp.strbrk s), info) in
         t_assign (`Exn e);
-        Hooks.(call execution_error start Loc.ghost (strbrk s));
+        execution_error start (Pp.strbrk s);
         feedback (InProgress ~-1)
 
-  let build_proof_here ~drop_pt (id,valid) loc eop =
+  let build_proof_here ?loc ~drop_pt (id,valid) eop =
     Future.create (State.exn_on id ~valid) (fun () ->
       let wall_clock1 = Unix.gettimeofday () in
-      if !Flags.batch_mode then Reach.known_state ~cache:`No eop
+      if VCS.is_interactive () = `No then Reach.known_state ~cache:`No eop
       else Reach.known_state ~cache:`Shallow eop;
       let wall_clock2 = Unix.gettimeofday () in
-      Aux_file.record_in_aux_at loc "proof_build_time"
+      Aux_file.record_in_aux_at ?loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       let p = Proof_global.return_proof ~allow_partial:drop_pt () in
-      if drop_pt then feedback ~id:(State id) Complete;
+      if drop_pt then feedback ~id Complete;
       p)
 
   let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1308,25 +1494,35 @@ end = struct (* {{{ *)
       VCS.print ();
       let proof, future_proof, time =
         let wall_clock = Unix.gettimeofday () in
-        let fp = build_proof_here ~drop_pt:drop exn_info loc stop in
+        let fp = build_proof_here ?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
        * the few errors tactics don't catch, like the "fix" tactic building
        * a bad fixpoint *)
       let fix_exn = Future.fix_exn_of future_proof in
+      (* STATE: We use the current installed imperative state *)
+      let st = Vernacstate.freeze_interp_state `No in
       if not drop then begin
-        let checked_proof = Future.chain ~pure:false future_proof (fun p ->
+        let checked_proof = Future.chain future_proof (fun p ->
+
+          (* Unfortunately close_future_proof and friends are not pure so we need
+             to set the state manually here *)
+          Vernacstate.unfreeze_interp_state st;
           let pobject, _ =
-            Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+            Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
-          vernac_interp stop
-            ~proof:(pobject, terminator)
+
+          let st = Vernacstate.freeze_interp_state `No in
+          stm_vernac_interp stop
+            ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = (VernacEndProof (Proved (Opaque None,None))) }) in
+              expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
+      (* STATE: Restore the state XXX: handle exn *)
+      Vernacstate.unfreeze_interp_state st;
       RespBuiltProof(proof,time)
     with
     | e when CErrors.noncritical e || e = Stack_overflow ->
@@ -1337,18 +1533,17 @@ end = struct (* {{{ *)
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        prerr_endline (fun () -> "failed with the following exception:");
-        prerr_endline (fun () -> string_of_ppcmds e_msg);
+        stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
         let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
-  
+
   let perform_states query =
     if query = [] then [] else
-    let is_tac e = match classify_vernac e with
+    let is_tac e = match Vernac_classifier.classify_vernac e with
     | VtProofStep _, _ -> true
     | _ -> false
     in
-    let initial = 
+    let initial =
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
         with VCS.Expired -> id in
@@ -1361,15 +1556,15 @@ end = struct (* {{{ *)
           then Some (prev, State.get_cached prev, step)
           else None
         with VCS.Expired -> None in
-      let this = 
+      let this =
         if State.is_cached_and_valid id then Some (State.get_cached id) else None in
       match prev, this with
       | _, None -> None
       | Some (prev, o, `Cmd { cast = { expr }}), Some n
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
-          Some (id, `Proof (prev, State.proof_part_of_frozen n))
+          Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_debug (str "STM: sending back a fat state");
+          msg_debug (Pp.str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
@@ -1385,13 +1580,14 @@ end = struct (* {{{ *)
     | ReqStates sl -> RespStates (perform_states sl)
 
   let on_marshal_error s = function
-    | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^
-        "The system state could not be sent to the master process."))
+    | States _ ->
+      msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+                             "The system state could not be sent to the master process."))
     | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
-      msg_error(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 ~drop_pt t_exn_info t_loc t_stop));
+      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));
       feedback (InProgress ~-1)
 
 end (* }}} *)
@@ -1401,13 +1597,13 @@ and Slaves : sig
 
   (* (eventually) remote calls *)
   val build_proof :
-    loc:Loc.t -> drop_pt:bool ->
+    ?loc:Loc.t -> drop_pt:bool ->
     exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t ->
-      name:string -> future_proof * cancel_switch
+      name:string -> future_proof * AsyncTaskQueue.cancel_switch
 
   (* blocking function that waits for the task queue to be empty *)
   val wait_all_done : unit -> unit
-  
+
   (* initialize the whole machinery (optional) *)
   val init : unit -> unit
 
@@ -1428,20 +1624,19 @@ and Slaves : sig
 
 end = struct (* {{{ *)
 
-  module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
-  
-  let queue = ref None
+  module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
 
+  let queue = ref None
   let init () =
-    if Flags.async_proofs_is_master () then
-      queue := Some (TaskQueue.create !Flags.async_proofs_n_workers)
+    if async_proofs_is_master !cur_opt then
+      queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers)
     else
       queue := Some (TaskQueue.create 0)
 
   let check_task_aux extra name l i =
     let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
     Flags.if_verbose msg_info
-      (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+      Pp.(str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
     VCS.restore document;
     let start =
       let rec aux cur =
@@ -1463,36 +1658,43 @@ end = struct (* {{{ *)
       (* 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;
-      vernac_interp stop ~proof
+      (* STATE SPEC:
+       * - start: First non-expired state! [This looks very fishy]
+       * - end  : start + qed
+       * => takes nothing from the itermediate states.
+       *)
+      (* STATE We use the state resulting from reaching start. *)
+      let st = Vernacstate.freeze_interp_state `No in
+      ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = (VernacEndProof (Proved (Opaque None,None))) };
+          expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
       `OK proof
       end
     with e ->
       let (e, info) = CErrors.push e in
       (try match Stateid.get info with
       | None ->
-          msg_error (
+        msg_warning Pp.(
             str"File " ++ str name ++ str ": proof of " ++ str r_name ++
             spc () ++ iprint (e, info))
       | Some (_, cur) ->
           match VCS.visit cur with
           | { step = `Cmd { cast = { loc } } }
-          | { step = `Fork (( { loc }, _, _, _), _) } 
-          | { step = `Qed ( { qast = { loc } }, _) } 
-          | { step = `Sideff (`Ast ( { loc }, _)) } ->
-              let start, stop = Loc.unloc loc in
-              msg_error (
+          | { step = `Fork (( { loc }, _, _, _), _) }
+          | { step = `Qed ( { qast = { loc } }, _) }
+          | { step = `Sideff (ReplayCommand { loc }, _) } ->
+              let start, stop = Option.cata Loc.unloc (0,0) loc in
+              msg_warning Pp.(
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
                 str ": chars " ++ int start ++ str "-" ++ int stop ++
                 spc () ++ iprint (e, info))
           | _ ->
-              msg_error (
+              msg_warning Pp.(
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
                 spc () ++ iprint (e, info))
     with e ->
-      msg_error (str"unable to print error message: " ++
-                    str (Printexc.to_string e)));
+      msg_warning Pp.(str"unable to print error message: " ++
+                      str (Printexc.to_string e)));
       if drop then `ERROR_ADMITTED else `ERROR
 
   let finish_task name (u,cst,_) d p l i =
@@ -1516,19 +1718,20 @@ end = struct (* {{{ *)
         let uc =
           Option.get
             (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        (** We only manipulate monomorphic terms here. *)
+        let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
         let pr =
-          Future.from_val (Option.get (Global.body_of_constant_body c)) in
+          Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
         let uc =
-          Future.chain
-            ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
-        let pr = Future.chain ~greedy:true ~pure:true pr discharge in
-        let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+          Future.chain uc Univ.hcons_universe_context_set in
+        let pr = Future.chain pr discharge in
+        let pr = Future.chain pr Constr.hcons in
         Future.sink pr;
         let extra = Future.join uc in
         u.(bucket) <- uc;
         p.(bucket) <- pr;
         u, Univ.ContextSet.union cst extra, false
-  
+
   let check_task name l i =
     match check_task_aux "" name l i with
     | `OK _ | `OK_ADMITTED -> true
@@ -1537,10 +1740,10 @@ end = struct (* {{{ *)
   let info_tasks l =
     CList.map_i (fun i ({ Stateid.loc; name }, _) ->
       let time1 =
-        try float_of_string (Aux_file.get !hints loc "proof_build_time")
+        try float_of_string (Aux_file.get ?loc !hints "proof_build_time")
         with Not_found -> 0.0 in
       let time2 =
-        try float_of_string (Aux_file.get !hints loc "proof_check_time")
+        try float_of_string (Aux_file.get ?loc !hints "proof_check_time")
         with Not_found -> 0.0 in
       name, max (time1 +. time2) 0.0001,i) 0 l
 
@@ -1561,11 +1764,11 @@ 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 ?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
-      if !Flags.compilation_mode = Flags.BuildVio then begin
+      if VCS.is_vio_doc () then begin
         let f,assign =
          Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
@@ -1573,11 +1776,11 @@ end = struct (* {{{ *)
           t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt;
           t_assign = assign; t_loc = loc; t_uuid; t_name = pname;
           t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in
-        TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
+        TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch;
         f, cancel_switch
       end else
-        ProofTask.build_proof_here ~drop_pt t_exn_info loc block_stop, cancel_switch
-    else 
+        ProofTask.build_proof_here ?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
       feedback (InProgress 1);
@@ -1585,7 +1788,7 @@ end = struct (* {{{ *)
         t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt;
         t_loc = loc; t_uuid; t_name = pname;
         t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in
-      TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
+      TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch;
       f, cancel_switch
 
   let wait_all_done () = TaskQueue.join (Option.get !queue)
@@ -1599,11 +1802,11 @@ end = struct (* {{{ *)
     let reqs =
       CList.map_filter
         ProofTask.(fun x ->
-             match request_of_task `Fresh x with
+             match request_of_task Fresh x with
              | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
-    prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
     reqs
 
   let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1612,7 +1815,7 @@ end (* }}} *)
 
 and TacTask : sig
 
-  type output = Constr.constr * Evd.evar_universe_context
+  type output = (Constr.constr * UState.t) option
   type task = {
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
@@ -1620,15 +1823,14 @@ and TacTask : sig
     t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
-    t_name     : string }  
-  exception NoProgress
+    t_name     : string }
 
   include AsyncTaskQueue.Task with type task := task
 
 end = struct (* {{{ *)
 
-  type output = Constr.constr * Evd.evar_universe_context
-  
+  type output = (Constr.constr * UState.t) option
+
   let forward_feedback msg = Hooks.(call forward_feedback msg)
 
   type task = {
@@ -1638,7 +1840,7 @@ end = struct (* {{{ *)
     t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
-    t_name     : string }  
+    t_name     : string }
 
   type request = {
     r_state    : Stateid.t;
@@ -1649,14 +1851,15 @@ end = struct (* {{{ *)
     r_name     : string }
 
   type response =
-    | RespBuiltSubProof of output
-    | RespError of std_ppcmds
+    | RespBuiltSubProof of (Constr.constr * UState.t)
+    | RespError of Pp.t
     | RespNoProgress
-  exception NoProgress
 
   let name = ref "tacworker"
   let extra_env () = [||]
   type competence = unit
+  type worker_status = Fresh | Old of competence
+
   let task_match _ _ = true
 
   (* run by the master, on a thread *)
@@ -1665,19 +1868,18 @@ end = struct (* {{{ *)
       r_state    = t_state;
       r_state_fb = t_state_fb;
       r_document =
-        if age <> `Fresh then None
+        if age <> Fresh then None
         else Some (VCS.slice ~block_start:t_state ~block_stop:t_state);
       r_ast      = t_ast;
       r_goal     = t_goal;
       r_name     = t_name }
     with VCS.Expired -> None
-          
+
   let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
     match resp with
-    | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+    | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
     | RespNoProgress ->
-        let e = (NoProgress, Exninfo.null) in
-        t_assign (`Exn e);
+        t_assign (`Val None);
         t_kill ();
         `Stay ((),[])
     | RespError msg ->
@@ -1685,15 +1887,15 @@ end = struct (* {{{ *)
         t_assign (`Exn e);
         t_kill ();
         `Stay ((),[])
-                    
+
   let on_marshal_error err { t_name } =
-    pr_err ("Fatal marshal error: " ^ t_name );
+    stm_pr_err ("Fatal marshal error: " ^ t_name );
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death = function
     | Some { t_kill } -> t_kill ()
     | _ -> ()
- 
+
   let command_focus = Proof.new_focus_kind ()
   let focus_cond = Proof.no_cond command_focus
 
@@ -1701,57 +1903,69 @@ end = struct (* {{{ *)
     Option.iter VCS.restore vcs;
     try
       Reach.known_state ~cache:`No id;
-      Future.purify (fun () ->
+      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
        if not (
-         Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
-         List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+         is_ground Evd.(evar_concl g) &&
+         List.for_all (Context.Named.Declaration.for_all is_ground)
                       Evd.(evar_context g))
        then
-         CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
+         CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
         let (i, ast) = r_ast in
         Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
-        vernac_interp r_state_fb ast;
+        (* STATE SPEC:
+         * - start : id
+         * - return: id
+         * => captures state id in a future closure, which will
+           discard execution state but for the proof + univs.
+        *)
+        let st = Vernacstate.freeze_interp_state `No in
+        ignore(stm_vernac_interp r_state_fb st ast);
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | 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
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
-            else CErrors.errorlabstrm "STM" (str"The solution is not ground")
+            else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground")
        end) ()
     with e when CErrors.noncritical e -> RespError (CErrors.print e)
 
   let name_of_task { t_name } = t_name
   let name_of_request { r_name } = r_name
-  
+
 end (* }}} *)
 
 and Partac : sig
 
   val vernac_interp :
-    solve:bool -> abstract:bool -> cancel_switch ->
-    int -> Stateid.t -> Stateid.t -> aast ->
-      unit
+    solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch ->
+    int -> Stateid.t -> Stateid.t -> aast -> unit
 
 end = struct (* {{{ *)
-    
-  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
 
-  let vernac_interp ~solve ~abstract cancel nworkers safe_id id
+  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
+
+  let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen }
   =
-    let e, time, fail =
-      let rec find time fail = function
-        | 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 () ->
-    (if time then System.with_time false else (fun x -> x)) (fun () ->
+    let e, time, batch, fail =
+      let rec find ~time ~batch ~fail = function
+        | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e
+        | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e
+        | VernacFail e -> find ~time ~batch ~fail:true e
+        | e -> e, time, batch, fail in
+      find ~time:false ~batch:false ~fail:false e in
+    let st = Vernacstate.freeze_interp_state `No in
+    Vernacentries.with_fail st fail (fun () ->
+    (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
       let goals, _, _, _, _ = Proof.proof p in
@@ -1764,19 +1978,19 @@ end = struct (* {{{ *)
         let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task queue
-          ({ t_state = safe_id; t_state_fb = id;
+          { t_state = safe_id; t_state_fb = id;
             t_assign = assign; t_ast; t_goal = g; t_name;
-            t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) },
-           cancel);
+            t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) }
+           ~cancel_switch;
         g,f)
         1 goals in
       TaskQueue.join queue;
       let assign_tac : unit Proofview.tactic =
-        Proofview.(Goal.nf_enter { Goal.enter = fun g ->
+        Proofview.(Goal.nf_enter begin fun g ->
         let gid = Goal.goal g in
         let f =
           try List.assoc gid res
-          with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in
+          with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in
         if not (Future.is_over f) then
           (* One has failed and cancelled the others, but not this one *)
           if solve then Tacticals.New.tclZEROMSG
@@ -1784,21 +1998,22 @@ end = struct (* {{{ *)
           else tclUNIT ()
         else
           let open Notations in
-          try
-            let pt, uc = Future.join f in
-            prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+          match Future.join f with
+          | Some (pt, uc) ->
+            let sigma, env = Pfedit.get_current_context () in
+            stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
-              str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
-              str"uc=" ++ Evd.pr_evar_universe_context uc)));
+              str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
+              str"uc=" ++ Termops.pr_evar_universe_context uc));
             (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
               (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
-              Tactics.exact_no_check pt)
-          with TacTask.NoProgress ->
+              Tactics.exact_no_check (EConstr.of_constr pt))
+          | None ->
             if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
-        })
+        end)
       in
       Proof.run_tactic (Global.env()) assign_tac p)))) ())
-  
+
 end (* }}} *)
 
 and QueryTask : sig
@@ -1807,10 +2022,10 @@ and QueryTask : sig
   include AsyncTaskQueue.Task with type task := task
 
 end = struct (* {{{ *)
-  
+
   type task =
     { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
-  
+
   type request =
     { r_where : Stateid.t ; r_for : Stateid.t ; r_what : aast; r_doc : VCS.vcs }
   type response = unit
@@ -1818,6 +2033,8 @@ end = struct (* {{{ *)
   let name = ref "queryworker"
   let extra_env _ = [||]
   type competence = unit
+  type worker_status = Fresh | Old of competence
+
   let task_match _ _ = true
 
   let request_of_task _ { t_where; t_what; t_for } =
@@ -1827,52 +2044,58 @@ end = struct (* {{{ *)
       r_doc   = VCS.slice ~block_start:t_where ~block_stop:t_where;
       r_what  = t_what }
     with VCS.Expired -> None
-  
+
   let use_response _ _ _ = `End
 
   let on_marshal_error _ _ =
-    pr_err ("Fatal marshal error in query");
+    stm_pr_err ("Fatal marshal error in query");
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death _ = ()
-  
+
   let forward_feedback msg = Hooks.(call forward_feedback msg)
 
   let perform { r_where; r_doc; r_what; r_for } =
     VCS.restore r_doc;
     VCS.print ();
     Reach.known_state ~cache:`No r_where;
+    (* STATE *)
+    let st = Vernacstate.freeze_interp_state `No in
     try
-      vernac_interp r_for { r_what with verbose = true };
-      feedback ~id:(State r_for) Processed
+      (* STATE SPEC:
+       * - start: r_where
+       * - end  : after execution of r_what
+       *)
+      ignore(stm_vernac_interp r_for st { r_what with verbose = true });
+      feedback ~id:r_for Processed
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
-      let msg = pp_to_richpp (iprint e) in
-      feedback ~id:(State r_for) (Message (Error, None, msg))
-    
+      let msg = iprint e     in
+      feedback ~id:r_for (Message (Error, None, msg))
+
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
 
 end (* }}} *)
 
-and Query : sig 
+and Query : sig
 
   val init : unit -> unit
-  val vernac_interp : cancel_switch -> Stateid.t ->  Stateid.t -> aast -> unit
+  val vernac_interp : cancel_switch:AsyncTaskQueue.cancel_switch -> Stateid.t ->  Stateid.t -> aast -> unit
 
 end = struct (* {{{ *)
 
-  module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask)
+  module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) ()
 
   let queue = ref None
 
-  let vernac_interp switch prev id q =
+  let vernac_interp ~cancel_switch prev id q =
     assert(TaskQueue.n_workers (Option.get !queue) > 0);
     TaskQueue.enqueue_task (Option.get !queue)
-      QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch)
+      QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
 
   let init () = queue := Some (TaskQueue.create
-    (if !Flags.async_proofs_full then 1 else 0))
+    (if !cur_opt.async_proofs_full then 1 else 0))
 
 end (* }}} *)
 
@@ -1884,21 +2107,18 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = summary_pstate
-
 let async_policy () =
-  let open Flags in
-  if is_universe_polymorphism () then false
-  else if interactive () = `Yes then
-    (async_proofs_is_master () || !async_proofs_mode = APonLazy)
+  if Flags.is_universe_polymorphism () then false
+  else if VCS.is_interactive () = `Yes then
+    (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
   else
-    (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
+    (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff)
 
 let delegate name =
-     get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
-  || !Flags.compilation_mode = Flags.BuildVio
-  || !Flags.async_proofs_full
- 
+     get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold
+  || VCS.is_vio_doc ()
+  || !cur_opt.async_proofs_full
+
 let warn_deprecated_nested_proofs =
   CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
          (fun () ->
@@ -1906,89 +2126,113 @@ let warn_deprecated_nested_proofs =
                     "stop working in a future Coq version"))
 
 let collect_proof keep cur hd brkind id =
- prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
  let name = function
    | [] -> no_name
-   | id :: _ -> Id.to_string id in
+   | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).loc in
- let is_defined = function
-   | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
-      true
+ let is_defined_expr = function
+   | VernacEndProof (Proved (Transparent,_)) -> true
    | _ -> false in
+ let is_defined = function
+   | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+                        && (not (Vernacprop.has_Fail e)) in
  let proof_using_ast = function
-   | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
+   | VernacProof(_,Some _) -> true
+   | _ -> false
+ in
+ let proof_using_ast = function
+   | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+                      && (not (Vernacprop.has_Fail v.expr)) -> Some v
    | _ -> None in
  let has_proof_using x = proof_using_ast x <> None in
  let proof_no_using = function
-   | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v
+   | VernacProof(t,None) -> t
+   | _ -> assert false
+ in
+ let proof_no_using = function
+   | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
    | _ -> assert false in
  let has_proof_no_using = function
-   | Some (_, { expr = VernacProof(_,None) }) -> true
+   | VernacProof(_,None) -> true
+   | _ -> false
+ in
+ let has_proof_no_using = function
+   | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+                    && (not (Vernacprop.has_Fail v.expr))
    | _ -> false in
  let too_complex_to_delegate = function
-   | { expr = (VernacDeclareModule _
-              | VernacDefineModule _
-              | VernacDeclareModuleType _
-              | VernacInclude _) } -> true
-   | { expr =  (VernacRequire _ | VernacImport _) } -> true
+   | VernacDeclareModule _
+   | VernacDefineModule _
+   | VernacDeclareModuleType _
+   | VernacInclude _
+   | VernacRequire _
+   | VernacImport _ -> true
    | ast -> may_pierce_opaque ast in
  let parent = function Some (p, _) -> p | None -> assert false in
- let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
+ let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
-    | (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
-      when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
+    | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
+      when too_complex_to_delegate (Vernacprop.under_control x.expr) ->
+       `Sync(no_name,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
-    | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
+    | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
-    | `Alias _ -> `Sync (no_name,None,`Alias)
+    | `Alias _ -> `Sync (no_name,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
-        `Sync (no_name,proof_using_ast last,`MutualProofs)
+        `Sync (no_name,`MutualProofs)
     | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) ->
-        `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity)
+        `Sync (no_name,`Doesn'tGuaranteeOpacity)
     | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
-        `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+        `ASync (parent last,accn,name,delegate name)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
        has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
-       !Flags.compilation_mode = Flags.BuildVio ->
+       VCS.is_vio_doc () ->
         assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
         (try
           let name, hint = name ids, get_hint_ctx loc  in
           let t, v = proof_no_using last in
-          v.expr <- VernacProof(t, Some hint);
-          `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+          v.expr <- VernacExpr([], VernacProof(t, Some hint));
+          `ASync (parent last,accn,name,delegate name)
         with Not_found ->
           let name = name ids in
-          `MaybeASync (parent last, None, accn, name, delegate name))
+          `MaybeASync (parent last, accn, name, delegate name))
     | `Fork((_, hd', GuaranteesOpacity, ids), _) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
-        `MaybeASync (parent last, None, accn, name, delegate name)
+        `MaybeASync (parent last, accn, name, delegate name)
     | `Sideff _ ->
        warn_deprecated_nested_proofs ();
-        `Sync (no_name,None,`NestedProof)
-    | _ -> `Sync (no_name,None,`Unknown) in
+        `Sync (no_name,`NestedProof)
+    | _ -> `Sync (no_name,`Unknown) in
  let make_sync why = function
-   | `Sync(name,pua,_) -> `Sync (name,pua,why)
-   | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why)
-   | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
+   | `Sync(name,_) -> `Sync (name,why)
+   | `MaybeASync(_,_,name,_) -> `Sync (name,why)
+   | `ASync(_,_,name,_) -> `Sync (name,why) in
+
  let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
+ let is_vernac_exact = function
+   | VernacExactProof _ -> true
+   | _ -> false
+ in
  match cur, (VCS.visit id).step, brkind with
- | (parent, { expr = VernacExactProof _ }), `Fork _, _ ->
-     `Sync (no_name,None,`Immediate)
+ | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+                                && (not (Vernacprop.has_Fail x.expr)) ->
+     `Sync (no_name,`Immediate)
  | _, _, { VCS.kind = `Edit _ }  -> check_policy (collect (Some cur) [] id)
  | _ ->
-     if is_defined cur then `Sync (no_name,None,`Transparent)
-     else if keep == VtDrop then `Sync (no_name,None,`Aborted)
+     if is_defined cur then `Sync (no_name,`Transparent)
+     else if keep == VtDrop then `Sync (no_name,`Aborted)
      else
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
        else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
-          (not(State.is_cached_and_valid id) || !Flags.async_proofs_full)
+          (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
@@ -2006,7 +2250,7 @@ let string_of_reason = function
   | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
   | `Unknown -> "unsupported case"
 
-let log_string s = prerr_debug (fun () -> "STM: " ^ s)
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
 let log_processing_async id name = log_string Printf.(sprintf
   "%s: proof %s: asynch" (Stateid.to_string id) name
 )
@@ -2018,7 +2262,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 error_absorbing_tactic id blockname exn =
     (* We keep the static/dynamic part of block detection separate, since
        the static part could be performed earlier.  As of today there is
@@ -2031,43 +2275,48 @@ let known_state ?(redefine_qed=false) ~cache id =
           Some (decl, name)
       | _ -> None) boxes in
     assert(List.length valid_boxes < 2);
-    if valid_boxes = [] then iraise exn
+    if valid_boxes = [] then Exninfo.iraise exn
     else
       let decl, name = List.hd valid_boxes in
       try
         let _, dynamic_check = List.assoc name !proof_block_delimiters in
-        match dynamic_check decl with
-        | `Leaks -> iraise exn
+        match dynamic_check dummy_doc decl with
+        | `Leaks -> Exninfo.iraise exn
         | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
            let tac =
-             let open Proofview.Notations in
-             Proofview.Goal.nf_enter { enter = fun gl ->
+             Proofview.Goal.nf_enter begin fun gl ->
                if CList.mem_f Evar.equal
                  (Proofview.Goal.goal gl) goals_to_admit then
              Proofview.give_up else Proofview.tclUNIT ()
-               } in
+              end in
            match (VCS.get_info base_state).state with
-           | Valid { proof } ->
+           | Valid { Vernacstate.proof } ->
                Proof_global.unfreeze proof;
                Proof_global.with_current_proof (fun _ p ->
-                 feedback ~id:(State id) Feedback.AddedAxiom;
+                 feedback ~id:id Feedback.AddedAxiom;
                  fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
-               Option.iter (fun expr -> vernac_interp id {
-                  verbose = true; loc = Loc.ghost; expr; indentation = 0;
-                  strlen = 0 })
+               (* STATE SPEC:
+                * - start: Modifies the input state adding a proof.
+                * - end  : maybe after recovery command.
+               *)
+               (* STATE: We use an updated state with proof *)
+               let st = Vernacstate.freeze_interp_state `No in
+               Option.iter (fun expr -> ignore(stm_vernac_interp id st {
+                  verbose = true; loc = None; expr; indentation = 0;
+                  strlen = 0 } ))
                recovery_command
            | _ -> assert false
         end
       with Not_found ->
-          CErrors.errorlabstrm "STM"
+          CErrors.user_err ~hdr:"STM"
             (str "Unknown proof block delimiter " ++ str name)
   in
 
   (* Absorb tactic errors from f () *)
   let resilient_tactic id blockname f =
-    if !Flags.async_proofs_tac_error_resilience = `None ||
-       (Flags.async_proofs_is_master () &&
-        !Flags.async_proofs_mode = Flags.APoff)
+    if !cur_opt.async_proofs_tac_error_resilience = `None ||
+       (async_proofs_is_master !cur_opt &&
+        !cur_opt.async_proofs_mode = APoff)
     then f ()
     else
       try f ()
@@ -2076,9 +2325,9 @@ let known_state ?(redefine_qed=false) ~cache id =
         error_absorbing_tactic id blockname ie in
   (* Absorb errors from f x *)
   let resilient_command f x =
-    if not !Flags.async_proofs_cmd_error_resilience ||
-       (Flags.async_proofs_is_master () &&
-        !Flags.async_proofs_mode = Flags.APoff)
+    if not !cur_opt.async_proofs_cmd_error_resilience ||
+       (async_proofs_is_master !cur_opt &&
+        !cur_opt.async_proofs_mode = APoff)
     then f x
     else
       try f x
@@ -2087,22 +2336,28 @@ let known_state ?(redefine_qed=false) ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
-    Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
-    Lib.freeze ~marshallable:`No in
+    let st = Summary.freeze_summaries ~marshallable:`No in
+    let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
+    let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
+    let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
+    st, Lib.freeze ~marshallable:`No in
+
   let inject_non_pstate (s,l) =
-    Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
+    Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
   in
-  let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
-    prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
-    reach ~safe_id id;
-    cherry_pick_non_pstate ()) id
+  let rec pure_cherry_pick_non_pstate safe_id id =
+    stm_purify (fun id ->
+        stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+        reach ~safe_id id;
+        cherry_pick_non_pstate ())
+      id
 
   (* traverses the dag backward from nodes being already calculated *)
   and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
-    prerr_endline (fun () -> "reaching: " ^ Stateid.to_string 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);
-      prerr_endline (fun () -> "reached (cache)");
+      stm_prerr_endline (fun () -> "reached (cache)");
       State.install_cached id
     end else
     let step, cache_step, feedback_processed =
@@ -2113,51 +2368,58 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
             reach view.next), cache, true
-      | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel); cblock } ->
+      | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } ->
           (fun () ->
             resilient_tactic id cblock (fun () ->
               reach ~cache:`Shallow view.next;
-              Hooks.(call tactic_being_run true); 
-              Partac.vernac_interp ~solve ~abstract
-                cancel !Flags.async_proofs_n_tacworkers view.next id x;
-              Hooks.(call tactic_being_run false))
+              Partac.vernac_interp ~solve ~abstract ~cancel_switch
+                !cur_opt.async_proofs_n_tacworkers view.next id x)
           ), cache, true
-      | `Cmd { cast = x; cqueue = `QueryQueue cancel }
-        when Flags.async_proofs_is_master () -> (fun () ->
+      | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
+        when async_proofs_is_master !cur_opt -> (fun () ->
             reach view.next;
-            Query.vernac_interp cancel view.next id x
+            Query.vernac_interp ~cancel_switch view.next id x
           ), cache, false
       | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
             resilient_tactic id cblock (fun () ->
               reach view.next;
-              Hooks.(call tactic_being_run true); 
-              vernac_interp id x;
-              Hooks.(call tactic_being_run false)); 
+              (* State resulting from reach *)
+              let st = Vernacstate.freeze_interp_state `No in
+              ignore(stm_vernac_interp id st x)
+            );
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
-            resilient_command reach view.next;
-            vernac_interp id x;
-	    if eff then update_global_env ()
-          ), (if eff then `Yes else cache), true
+          (match !cur_opt.async_proofs_mode with
+           | APon | APonLazy ->
+             resilient_command reach view.next
+           | APoff -> reach view.next);
+          let st = Vernacstate.freeze_interp_state `No in
+          ignore(stm_vernac_interp id st x);
+          if eff then update_global_env ()
+        ), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             resilient_command reach view.next;
-            vernac_interp id x;
+            let st = Vernacstate.freeze_interp_state `No in
+            ignore(stm_vernac_interp id st x);
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
       | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
             reach ~cache:`Shallow prev;
             reach view.next;
-            (try vernac_interp id x;
+
+            (try
+               let st = Vernacstate.freeze_interp_state `No in
+               ignore(stm_vernac_interp id st x);
             with e when CErrors.noncritical e ->
               let (e, info) = CErrors.push e in
               let info = Stateid.add info ~valid:prev id in
-              iraise (e, info));
+              Exninfo.iraise (e, info));
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
-          | `ASync (block_start, pua, nodes, name, delegate) -> (fun () ->
+          | `ASync (block_start, nodes, name, delegate) -> (fun () ->
                 assert(keep == VtKeep || keep == VtKeepAsAxiom);
                 let drop_pt = keep == VtKeepAsAxiom in
                 let block_stop, exn_info, loc = eop, (id, eop), x.loc in
@@ -2168,7 +2430,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
                     if okeep != keep then
-                      msg_error(strbrk("The command closing the proof changed. "
+                      msg_warning(strbrk("The command closing the proof changed. "
                         ^"The kernel cannot take this into account and will "
                         ^(if keep == VtKeep then "not check " else "reject ")
                         ^"the "^(if keep == VtKeep then "new" else "incomplete")
@@ -2176,7 +2438,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                         ^"the proof's statement to avoid that."));
                     let fp, cancel =
                       Slaves.build_proof
-                        ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
+                        ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
                     Future.replace ofp fp;
                     qed.fproof <- Some (fp, cancel);
                     (* We don't generate a new state, but we still need
@@ -2188,35 +2450,39 @@ let known_state ?(redefine_qed=false) ~cache id =
                     let fp, cancel =
                       if delegate then
                         Slaves.build_proof
-                          ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
+                          ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
                       else
-                        ProofTask.build_proof_here
-                          ~drop_pt exn_info loc block_stop, ref false
+                        ProofTask.build_proof_here ?loc
+                          ~drop_pt exn_info block_stop, ref false
                     in
                     qed.fproof <- Some (fp, cancel);
                     let proof =
                       Proof_global.close_future_proof ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
-                    vernac_interp id ~proof x;
-                    feedback ~id:(State id) Incomplete
+                    let st = Vernacstate.freeze_interp_state `No in
+                    ignore(stm_vernac_interp id ~proof st x);
+                    feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
                 Proof_global.discard_all ()
               ), (if redefine_qed then `No else `Yes), true
-          | `Sync (name, _, `Immediate) -> (fun () -> 
-                reach eop; vernac_interp id x; Proof_global.discard_all ()
+          | `Sync (name, `Immediate) -> (fun () ->
+                reach eop;
+                let st = Vernacstate.freeze_interp_state `No in
+                ignore(stm_vernac_interp id st x);
+                Proof_global.discard_all ()
               ), `Yes, true
-          | `Sync (name, pua, reason) -> (fun () ->
+          | `Sync (name, reason) -> (fun () ->
                 log_processing_sync id name reason;
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
-                record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
+                record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork);
                 let proof =
                   match keep with
                   | VtDrop -> None
                   | VtKeepAsAxiom ->
-                      let ctx = Evd.empty_evar_universe_context in
+                      let ctx = UState.empty in
                       let fp = Future.from_val ([],ctx) in
                       qed.fproof <- Some (fp, ref false); None
                   | VtKeep ->
@@ -2226,52 +2492,132 @@ let known_state ?(redefine_qed=false) ~cache id =
                 if keep != VtKeepAsAxiom then
                   reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
-                vernac_interp id ?proof x;
+                let st = Vernacstate.freeze_interp_state `No in
+                ignore(stm_vernac_interp id ?proof st x);
                 let wall_clock3 = Unix.gettimeofday () in
-                Aux_file.record_in_aux_at x.loc "proof_check_time"
+                Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
                 Proof_global.discard_all ()
               ), `Yes, true
-          | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
+          | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
                 reach ~cache:`Shallow start;
                 (* no sections *)
-                if List.is_empty (Environ.named_context (Global.env ()))
-                then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
-                else pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
+                if CList.is_empty (Environ.named_context (Global.env ()))
+                then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
+                else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
               ), (if redefine_qed then `No else `Yes), true
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
-      | `Sideff (`Ast (x,_)) -> (fun () ->
-            reach view.next; vernac_interp id x; update_global_env ()
+      | `Sideff (ReplayCommand x,_) -> (fun () ->
+            reach view.next;
+            let st = Vernacstate.freeze_interp_state `No in
+            ignore(stm_vernac_interp id st x);
+            update_global_env ()
           ), cache, true
-      | `Sideff (`Id origin) -> (fun () ->
+      | `Sideff (CherryPickEnv, origin) -> (fun () ->
             reach view.next;
             inject_non_pstate (pure_cherry_pick_non_pstate view.next origin);
           ), cache, true
     in
     let cache_step =
-      if !Flags.async_proofs_cache = Some Flags.Force then `Yes
+      if !cur_opt.async_proofs_cache = Some Force then `Yes
       else cache_step in
     State.define ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+    stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
 end (* }}} *)
+[@@@ocaml.warning "+60"]
 
 (********************************* STM API ************************************)
 (******************************************************************************)
 
-let init () =
-  VCS.init Stateid.initial;
-  set_undo_classifier Backtrack.undo_vernac_classifier;
-  State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
+(* Main initalization routine *)
+type stm_init_options = {
+  (* The STM will set some internal flags differently depending on the
+     specified [doc_type]. This distinction should dissappear at some
+     some point. *)
+  doc_type     : stm_doc_type;
+
+  (* Initial load path in scope for the document. Usually extracted
+     from -R options / _CoqProject *)
+  iload_path   : Mltop.coq_path list;
+
+  (* Require [require_libs] before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  require_libs : (string * string option * bool option) list;
+
+  (* STM options that apply to the current document. *)
+  stm_options  : AsyncOpts.stm_opt;
+}
+(* fb_handler   : Feedback.feedback -> unit; *)
+
+(*
+let doc_type_module_name (std : stm_doc_type) =
+  match std with
+  | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn
+  | Interactive mn -> Names.DirPath.to_string mn
+*)
+
+let init_core () =
+  if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
+  State.register_root_state ()
+
+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
+      Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
+    List.(iter rq_file (rev libs))
+  in
+
+  (* Set the options from the new documents *)
+  AsyncOpts.cur_opt := stm_options;
+
+  (* We must reset the whole state before creating a document! *)
+  State.restore_root_state ();
+
+  let doc = VCS.init doc_type Stateid.initial in
+
+  (* Set load path; important, this has to happen before we declare
+     the library below as [Declaremods/Library] will infer the module
+     name by looking at the load path! *)
+  List.iter Mltop.add_coq_path iload_path;
+
+  begin match doc_type with
+  | Interactive ln ->
+    Safe_typing.allow_delayed_constants := true;
+    Declaremods.start_library ln
+
+  | VoDoc ln ->
+    let ldir = Flags.verbosely Library.start_library ln in
+    VCS.set_ldir ldir;
+    set_compilation_hints ln
+
+  | VioDoc ln ->
+    Safe_typing.allow_delayed_constants := true;
+    let ldir = Flags.verbosely Library.start_library ln in
+    VCS.set_ldir ldir;
+    set_compilation_hints ln
+  end;
+
+  (* Import initial libraries. *)
+  load_objs require_libs;
+
+  (* We record the state at this point! *)
+  State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
-  if Flags.async_proofs_is_master () then begin
-    prerr_endline (fun () -> "Initializing workers");
+  if async_proofs_is_master !cur_opt then begin
+    stm_prerr_endline (fun () -> "Initializing workers");
     Query.init ();
-    let opts = match !Flags.async_proofs_private_flags with
+    let opts = match !cur_opt.async_proofs_private_flags with
       | None -> []
       | Some s -> Str.split_delim (Str.regexp ",") s in
     begin try
@@ -2280,34 +2626,39 @@ let init () =
       async_proofs_workers_extra_env := Array.of_list
         (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
     with Not_found -> () end;
-  end
+  end;
+  doc, VCS.cur_tip ()
 
-let observe id =
+let observe ~doc id =
   let vcs = VCS.backup () in
   try
-    Reach.known_state ~cache:(interactive ()) id;
-    VCS.print ()
+    Reach.known_state ~cache:(VCS.is_interactive ()) id;
+    VCS.print ();
+    doc
   with e ->
     let e = CErrors.push e in
     VCS.print ();
     VCS.restore vcs;
-    iraise e
+    Exninfo.iraise e
 
-let finish ?(print_goals=false) () =
+let finish ~doc =
   let head = VCS.current_branch () in
-  observe (VCS.get_branch_pos head);
-  if print_goals then msg_notice (pr_open_cur_subgoals ());
+  let doc =observe ~doc (VCS.get_branch_pos head) in
   VCS.print ();
+  (* EJGA: Setting here the proof state looks really wrong, and it
+     hides true bugs cf bug #5363. Also, what happens with observe? *)
   (* Some commands may by side effect change the proof mode *)
-  match VCS.get_branch head with
-  | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
-  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+  (match VCS.get_branch head with
+  | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
+  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
   | _ -> ()
+  ); doc
 
-
-let wait () =
+let wait ~doc =
+  let doc = finish ~doc in
   Slaves.wait_all_done ();
-  VCS.print ()
+  VCS.print ();
+  doc
 
 let rec join_admitted_proofs id =
   if Stateid.equal id Stateid.initial then () else
@@ -2318,33 +2669,33 @@ let rec join_admitted_proofs id =
        join_admitted_proofs view.next
   | _ -> join_admitted_proofs view.next
 
-let join () =
-  finish ();
-  wait ();
-  prerr_endline (fun () -> "Joining the environment");
+let join ~doc =
+  let doc = wait ~doc in
+  stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
-  prerr_endline (fun () -> "Joining Admitted proofs");
+  stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
-  VCS.print ()
+  doc
 
 let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
-type document = VCS.vcs
+
 type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
 let check_task name (tasks,rcbackup) i =
   RemoteCounter.restore rcbackup;
   let vcs = VCS.backup () in
   try
-    let rc = Future.purify (Slaves.check_task name tasks) i in
+    let rc = stm_purify (Slaves.check_task name tasks) i in
     VCS.restore vcs;
     rc
   with e when CErrors.noncritical e -> VCS.restore vcs; false
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
+
 let finish_tasks name u d p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
   let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
-    let u = Future.purify (Slaves.finish_task name u d p t) i in
+    let u = stm_purify (Slaves.finish_task name u d p t) i in
     VCS.restore vcs;
     u in
   try
@@ -2352,7 +2703,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     (u,a,true), p
   with e ->
     let e = CErrors.push e in
-    msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+    msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
 let merge_proof_branch ~valid ?id qast keep brname =
@@ -2364,7 +2715,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       let id = VCS.new_node ?id () in
       VCS.merge id ~ours:(Qed (qed None)) brname;
       VCS.delete_branch brname;
-      VCS.propagate_sideff None;
+      VCS.propagate_sideff ~action:CherryPickEnv;
       `Ok
   | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
       let ofp =
@@ -2374,130 +2725,113 @@ 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 ();
-      Reach.known_state ~redefine_qed:true ~cache:`No qed_id;
+      let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
-       iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+       Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
 
 (* 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 tty =
-  if e = CErrors.Drop then iraise (e, info) else
+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;
       VCS.print ();
-      if tty && interactive () = `Yes then begin
-        (* Hopefully the 1 to last state is valid *)
-        Backtrack.back_safe (); 
-        VCS.checkout_shallowest_proof_branch ();
-      end;
-      VCS.print ();
       anomaly(str"error with no safe_id attached:" ++ spc() ++
-        CErrors.iprint_no_report (e, info))
+        CErrors.iprint_no_report (e, info) ++ str".")
   | Some (safe_id, id) ->
-      prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+      stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
-      if tty && interactive () = `Yes then begin
-        (* We stay on a valid state *)
-        Backtrack.backto safe_id;
-        VCS.checkout_shallowest_proof_branch ();
-        Reach.known_state ~cache:(interactive ()) safe_id;
-      end;
       VCS.print ();
-      iraise (e, info)
+      Exninfo.iraise (e, info)
 
-let snapshot_vio ldir long_f_dot_vo =
-  finish ();
+let snapshot_vio ~doc ldir long_f_dot_vo =
+  let doc = finish ~doc in
   if List.length (VCS.branches ()) > 1 then
-    CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+    CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
-    (Global.opaque_tables ())
+    (Global.opaque_tables ());
+  doc
 
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
+  match part_of_script, w with
+  | true, 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
+    List.iter (fun branch ->
+        if not (List.mem_assoc branch (mine::others)) then
+          ignore(merge_proof_branch ~valid aast VtDrop branch))
+      (VCS.branches ());
+    VCS.checkout_shallowest_proof_branch ();
+    let head = VCS.current_branch () in
+    List.iter (fun b ->
+        if not(VCS.Branch.equal b head) then begin
+          VCS.checkout b;
+          VCS.commit (VCS.new_node ()) (Alias (oid,aast));
+        end)
+      (VCS.branches ());
+    VCS.checkout_shallowest_proof_branch ();
+    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 process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
   ({ verbose; loc; expr } as x) c =
-  prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
   try
     let head = VCS.current_branch () in
     VCS.checkout head;
     let rc = begin
-      prerr_endline (fun () ->
-        "  classified as: " ^ string_of_vernac_classification c);
+      stm_prerr_endline (fun () ->
+        "  classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
       match c with
-      (* PG stuff *)    
-      | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
-      | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
-      (* Joining various parts of the document *)
-      | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
-      | VtStm (VtFinish, b),       VtNow -> finish (); `Ok
-      | VtStm (VtWait, b),     VtNow -> finish (); wait (); `Ok
-      | VtStm (VtPrintDag, b), VtNow ->
-          VCS.print ~now:true (); `Ok
-      | VtStm (VtObserve id, b),   VtNow -> observe id; `Ok
-      | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
-                |VtPrintDag |VtWait),_), VtLater ->
-          anomaly(str"classifier: join actions cannot be classified as VtLater")
-      
-      (* Back *)
-      | VtStm (VtBack oid, true), 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
-          List.iter (fun branch ->
-            if not (List.mem_assoc branch (mine::others)) then
-              ignore(merge_proof_branch ~valid x VtDrop branch))
-            (VCS.branches ());
-          VCS.checkout_shallowest_proof_branch ();
-          let head = VCS.current_branch () in
-          List.iter (fun b ->
-            if not(VCS.Branch.equal b head) then begin
-              VCS.checkout b;
-              VCS.commit (VCS.new_node ()) (Alias (oid,x));
-            end)
-            (VCS.branches ());
-          VCS.checkout_shallowest_proof_branch ();
-          VCS.commit id (Alias (oid,x));
-          Backtrack.record (); if w == VtNow then finish (); `Ok
-      | VtStm (VtBack id, false), VtNow ->
-          prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
-          Backtrack.backto id;
-          VCS.checkout_shallowest_proof_branch ();
-          Reach.known_state ~cache:(interactive ()) id; `Ok
-      | VtStm (VtBack id, false), VtLater ->
-          anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
-
+      (* 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
       (* Query *)
-      | VtQuery (false,(report_id,route)), VtNow when tty = true ->
-          finish ();
-          (try Future.purify (vernac_interp report_id ~route)
-            {x with verbose = true }
-           with e when CErrors.noncritical e ->
-             let e = CErrors.push e in
-             iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
-      | VtQuery (false,(report_id,route)), VtNow ->
-          (try vernac_interp report_id ~route x
-           with e ->
-             let e = CErrors.push e in
-             iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
-      | VtQuery (true,(report_id,_)), w ->
-          assert(Stateid.equal report_id Stateid.dummy);
+      | 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 ->
           let id = VCS.new_node ~id:newtip () in
           let queue =
-            if !Flags.async_proofs_full then `QueryQueue (ref false)
-            else if Flags.(!compilation_mode = BuildVio) &&
+            if !cur_opt.async_proofs_full then `QueryQueue (ref false)
+            else if VCS.is_vio_doc () &&
                     VCS.((get_branch head).kind = `Master) &&
-                    may_pierce_opaque x
-                 then `SkipQueue 
+                    may_pierce_opaque (Vernacprop.under_control x.expr)
+                 then `SkipQueue
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          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")
+          anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
 
       (* Proof *)
       | VtStartProof (mode, guarantee, names), w ->
@@ -2511,10 +2845,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
             VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
             VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
           end;
-          Proof_global.activate_proof_mode mode;
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
       | VtProofMode _, VtLater ->
-          anomaly(str"VtProofMode must be executed VtNow")
+          anomaly(str"VtProofMode must be executed VtNow.")
       | VtProofMode mode, VtNow ->
           let id = VCS.new_node ~id:newtip () in
           VCS.commit id (mkTransCmd x [] false `MainQueue);
@@ -2530,7 +2864,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record ();
-          finish ();
+          ignore(finish ~doc:dummy_doc);
           `Ok
       | VtProofStep { parallel; proof_block_detection = cblock }, w ->
           let id = VCS.new_node ~id:newtip () in
@@ -2543,121 +2877,192 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
              If/when and UI will make something useful with this piece of info,
              detection should occur here.
           detect_proof_block id cblock; *)
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
       | VtQed keep, w ->
           let valid = VCS.get_branch_pos head in
           let rc = merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w == VtNow then finish ();
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
           rc
-          
-      (* Side effect on all branches *)
-      | VtUnknown, _ when expr = VernacToplevelControl Drop ->
-          vernac_interp (VCS.get_branch_pos head) x; `Ok
+
+      (* 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
 
       | VtSideff l, w ->
-          let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
-          VCS.checkout VCS.Branch.master;
-          VCS.commit id (mkTransCmd x l in_proof `MainQueue);
-          (* We can't replay a Definition since universes may be differently
-           * inferred.  This holds in Coq >= 8.5 *)
-	  let replay = match x.expr with
-	    | VernacDefinition(_, _, DefineBody _) -> None
-	    | _ -> Some x in
-	  VCS.propagate_sideff ~replay;
+          begin match (VCS.get_branch head).VCS.kind with
+          | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue);
+          | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue);
+          | `Proof _ ->
+              VCS.checkout VCS.Branch.master;
+              VCS.commit id (mkTransCmd x l true `MainQueue);
+              (* We can't replay a Definition since universes may be differently
+               * inferred.  This holds in Coq >= 8.5 *)
+              let action = match Vernacprop.under_control x.expr with
+                | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
+                | _ -> ReplayCommand x in
+              VCS.propagate_sideff ~action;
+          end;
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w == VtNow then finish (); `Ok
+          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
       (* Unknown: we execute it, check for open goals and propagate sideeff *)
       | VtUnknown, VtNow ->
           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
-          Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
+          let _st = Reach.known_state ~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
-            Reach.known_state ~cache:(interactive ()) mid;
-            vernac_interp id x;
+            let _st' = Reach.known_state ~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 *)
             if not in_proof && Proof_global.there_are_pending_proofs () then
             begin
               let bname = VCS.mk_branch_name x in
-              let opacity_of_produced_term =
-                match x.expr with
+              let opacity_of_produced_term = function
                 (* This AST is ambiguous, hence we check it dynamically *)
                 | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
                 | _ -> Doesn'tGuaranteeOpacity in
-              VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
+              VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
               let proof_mode = default_proof_mode () in
               VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
-              Proof_global.activate_proof_mode proof_mode;
+              Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
             end else begin
-              VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              (* We hope it can be replayed, but we can't really know *)
-              VCS.propagate_sideff ~replay:(Some x);
+              begin match (VCS.get_branch head).VCS.kind with
+              | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+              | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+              | `Proof _ ->
+                  VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+                  (* We hope it can be replayed, but we can't really know *)
+                  VCS.propagate_sideff ~action:(ReplayCommand x);
+              end;
               VCS.checkout_shallowest_proof_branch ();
             end in
           State.define ~safe_id:head_id ~cache:`Yes step id;
           Backtrack.record (); `Ok
 
       | VtUnknown, VtLater ->
-          anomaly(str"classifier: VtUnknown must imply VtNow")
+          anomaly(str"classifier: VtUnknown must imply VtNow.")
     end in
-    (* Proof General *)
-    begin match expr with 
-      | VernacStm (PGLast _) ->
-        if not (VCS.Branch.equal head VCS.Branch.master) then
-          vernac_interp Stateid.dummy
-            { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
-              expr = VernacShow (ShowGoal OpenSubgoals) }
-      | _ -> ()
-    end;
-    prerr_endline (fun () -> "processed }}}");
+    let pr_rc rc = match rc with
+      | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
+      | _   -> Pp.(str "unfocus")
+    in
+    stm_pperr_endline (fun () -> str "processed with " ++ pr_rc rc ++ str " }}}");
     VCS.print ();
     rc
   with e ->
     let e = CErrors.push e in
-    handle_failure e vcs tty
+    handle_failure e vcs
 
-let get_ast id =
+let get_ast ~doc id =
   match VCS.visit id with
   | { step = `Cmd { cast = { loc; expr } } }
-  | { step = `Fork (({ loc; expr }, _, _, _), _) } 
+  | { step = `Fork (({ loc; expr }, _, _, _), _) }
+  | { step = `Sideff ((ReplayCommand {loc; expr}) , _) }
   | { step = `Qed ({ qast = { loc; expr } }, _) } ->
-         Some (expr, loc)
+         Some (Loc.tag ?loc expr)
   | _ -> None
 
 let stop_worker n = Slaves.cancel_worker n
 
+(* We must parse on top of a state id, it should be something like:
+
+   - get parsing information for that state.
+   - feed the parsable / parser with the right parsing information.
+   - call the parser
+
+   Now, the invariant in ensured by the callers, but this is a bit
+   problematic.
+*)
+exception End_of_input
+
+let parse_sentence ~doc sid pa =
+  (* XXX: Should this restore the previous state?
+     Using reach here to try to really get to the
+     proper state makes the error resilience code fail *)
+  (* Reach.known_state ~cache:`Yes sid; *)
+  let cur_tip = VCS.cur_tip () in
+  let real_tip = !State.cur_id in
+  if not (Stateid.equal sid cur_tip) then
+    user_err ~hdr:"Stm.parse_sentence"
+      (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
+       str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
+       str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
+  if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then
+    Feedback.msg_debug
+      (str "Warning, the real tip doesn't match the current tip." ++
+       str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
+       str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++
+       str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++
+       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
+        | None            -> raise End_of_input
+        | Some (loc, cmd) -> CAst.make ~loc cmd
+      with e when CErrors.noncritical e ->
+        let (e, info) = CErrors.push e in
+        Exninfo.iraise (e, info))
+    ()
+
 (* You may need to know the len + indentation of previous command to compute
  * the indentation of the current one.
  *  Eg.   foo. bar.
  * Here bar is indented of the indentation of foo + its strlen (4) *)
-let ind_len_of id =
-  if Stateid.equal id Stateid.initial then 0
-  else match (VCS.visit id).step with
-  | `Cmd { ctac = true; cast = { indentation; strlen } } ->
-       indentation + strlen
-  | _ -> 0
-
-let add ~ontop ?newtip ?(check=ignore) verb eid s =
+let ind_len_loc_of_id sid =
+  if Stateid.equal sid Stateid.initial then None
+  else match (VCS.visit sid).step with
+  | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
+         Some (indentation, strlen, loc)
+  | _ -> None
+
+(* the indentation logic works like this: if the beginning of the
+   command is different than the start we are in a new line, thus
+   indentation follows from the starting position. Otherwise, we use
+   the previous one plus the offset.
+
+   Note, this could maybe improved by handling more cases in
+   compute_indentation. *)
+
+let compute_indentation ?loc sid = Option.cata (fun loc ->
+  let open Loc              in
+  (* The effective lenght is the lenght on the last line *)
+  let len = loc.ep - loc.bp in
+  let prev_indent = match ind_len_loc_of_id sid with
+    | None         -> 0
+    | Some (i,l,p) -> i + l
+  in
+  (* Now if the line has not changed, the need to add the previous indent *)
+  let eff_indent = loc.bp - loc.bol_pos in
+  if loc.bol_pos = 0 then
+    eff_indent + prev_indent, len
+  else
+    eff_indent, len
+  ) (0, 0) loc
+
+let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
-    (* For now, arbitrary edits should be announced with edit_at *)
-    anomaly(str"Not yet implemented, the GUI should not try this");
-  let indentation, strlen, loc, ast =
-    vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
-  CWarnings.set_current_loc loc;
-  check(loc,ast);
-  let clas = classify_vernac ast in
+    user_err ?loc ~hdr:"Stm.add"
+      (str "Stm.add called for a different state (" ++ str (Stateid.to_string ontop) ++
+       str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++
+       str "This is not supported yet, sorry.");
+  let indentation, strlen = compute_indentation ?loc ontop in
+  (* 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 ~tty:false aast clas with
-  | `Ok -> VCS.cur_tip (), `NewTip
-  | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
+  match process_transaction ?newtip aast clas with
+  | `Ok -> doc, VCS.cur_tip (), `NewTip
+  | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
 
-let set_perspective id_list = Slaves.set_perspective id_list
+let set_perspective ~doc id_list = Slaves.set_perspective id_list
 
 type focus = {
   start : Stateid.t;
@@ -2665,25 +3070,32 @@ type focus = {
   tip : Stateid.t
 }
 
-let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
-  Future.purify (fun s ->
-    if Stateid.equal at Stateid.dummy then finish ()
+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;
-    let newtip, route = report_with in
-    let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
-    CWarnings.set_current_loc loc;
-    let clas = classify_vernac ast in
-    let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
-    match clas with
-    | VtStm (w,_), _ ->
-       ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
-    | _ ->
-       ignore(process_transaction
-         ~tty:false aast (VtQuery (false,report_with), VtNow)))
+    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 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))
+      done;
+    with
+    | End_of_input -> ()
+    | exn ->
+      let iexn = CErrors.push exn in
+      Exninfo.iraise iexn
+    )
   s
 
-let edit_at id =
-  if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else
+let edit_at ~doc id =
+  if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else
   let vcs = VCS.backup () in
   let on_cur_branch id =
     let rec aux cur =
@@ -2714,7 +3126,7 @@ let edit_at id =
       if Stateid.equal tip Stateid.initial then tip else
       match VCS.visit tip with
       | { step = (`Fork _ | `Qed _) } -> tip
-      | { step = `Sideff (`Ast(_,id)) } -> id
+      | { step = `Sideff (ReplayCommand _,id) } -> id
       | { step = `Sideff _ } -> tip
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip old_branch =
@@ -2722,12 +3134,12 @@ let edit_at id =
       (* Hum, this should be the real start_id in the cluster and not next *)
       match VCS.visit qed_id with
       | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
-      | _ -> anomaly (str "ProofTask not ending with Qed") in
+      | _ -> anomaly (str "ProofTask not ending with Qed.") in
     VCS.branch ~root:master_id ~pos: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:(interactive ()) id;
+    Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `Focus { stop = qed_id; start = master_id; tip } in
   let no_edit = function
@@ -2749,8 +3161,8 @@ let edit_at id =
     VCS.delete_boxes_of id;
     VCS.gc ();
     VCS.print ();
-    if not !Flags.async_proofs_full then
-      Reach.known_state ~cache:(interactive ()) id;
+    if not !cur_opt.async_proofs_full then
+      Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
@@ -2765,7 +3177,7 @@ let edit_at id =
       | _, Some _, None -> assert false
       | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
           let tip = VCS.cur_tip () in
-          if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
+          if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch
           then reopen_branch start id mode qed_id tip bn
           else backto id (Some bn)
       | true, Some { qed = qed_id }, Some(mode,bn) ->
@@ -2774,67 +3186,46 @@ let edit_at id =
           end else if is_ancestor_of_cur_branch id then begin
             backto id (Some bn)
           end else begin
-            anomaly(str"Cannot leave an `Edit branch open")
+            anomaly(str"Cannot leave an `Edit branch open.")
           end
       | true, None, _ ->
           if on_cur_branch id then begin
             VCS.reset_branch (VCS.current_branch ()) id;
-            Reach.known_state ~cache:(interactive ()) id;
+            Reach.known_state ~cache:(VCS.is_interactive ()) id;
             VCS.checkout_shallowest_proof_branch ();
             `NewTip
           end else if is_ancestor_of_cur_branch id then begin
             backto id None
           end else begin
-            anomaly(str"Cannot leave an `Edit branch open")
+            anomaly(str"Cannot leave an `Edit branch open.")
           end
       | false, None, Some(_,bn) -> backto id (Some bn)
       | false, None, None -> backto id None
     in
     VCS.print ();
-    rc
+    doc, rc
   with e ->
     let (e, info) = CErrors.push e in
     match Stateid.get info with
     | None ->
         VCS.print ();
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
-          CErrors.print_no_report e)
+          CErrors.print_no_report e ++ str ".")
     | Some (_, id) ->
-        prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+        stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
-        iraise (e, info)
+        Exninfo.iraise (e, info)
 
-let backup () = VCS.backup ()
-let restore d = VCS.restore d
+let get_current_state ~doc = VCS.cur_tip ()
+let get_ldir ~doc = VCS.get_ldir ()
+
+let get_doc did = dummy_doc
 
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
-let interp verb (loc,e) =
-  let clas = classify_vernac e in
-  let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in
-  let rc = process_transaction ~tty:true aast clas in
-  if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
-  if interactive () = `Yes ||
-     (!Flags.async_proofs_mode = Flags.APoff &&
-      !Flags.compilation_mode = Flags.BuildVo) then
-    let vcs = VCS.backup () in
-    let print_goals =
-      verb && match clas with
-       | VtQuery _, _ -> false
-       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
-       | _ -> not !Flags.coqtop_ui in
-    try finish ~print_goals ()
-    with e ->
-      let e = CErrors.push e in
-      handle_failure e vcs true
-
-let finish () = finish ()
-
-let get_current_state () = VCS.cur_tip ()
-
-let current_proof_depth () =
+let current_proof_depth ~doc =
   let head = VCS.current_branch () in
   match VCS.get_branch head with
   | { VCS.kind = `Master } -> 0
@@ -2847,111 +3238,25 @@ let current_proof_depth () =
 let unmangle n =
   let n = VCS.Branch.to_string n in
   let idx = String.index n '_' + 1 in
-  Names.id_of_string (String.sub n idx (String.length n - idx))
+  Names.Id.of_string (String.sub n idx (String.length n - idx))
 
 let proofname b = match VCS.get_branch b with
   | { VCS.kind = (`Proof _| `Edit _) } -> Some b
   | _ -> None
 
-let get_all_proof_names () =
-  List.map unmangle (List.map_filter proofname (VCS.branches ()))
-
-let get_current_proof_name () =
-  Option.map unmangle (proofname (VCS.current_branch ()))
-
-let get_script prf =
-  let branch, test =
-    match prf with
-    | None -> VCS.Branch.master, fun _ -> true
-    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
-  let rec find acc id =
-    if Stateid.equal id Stateid.initial ||
-       Stateid.equal id Stateid.dummy then acc else
-    let view = VCS.visit id in
-    match view.step with
-    | `Fork((_,_,_,ns), _) when test ns -> acc
-    | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
-    | `Sideff (`Ast (x,_)) ->
-         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
-    | `Sideff (`Id id)  -> find acc id
-    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
-         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
-    | `Cmd _ -> find acc view.next
-    | `Alias (id,_) -> find acc id
-    | `Fork _ -> find acc view.next
-    in
-  find [] (VCS.get_branch_pos branch)
-
-(* indentation code for Show Script, initially contributed
-   by D. de Rauglaudre *)
-
-let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
-  (* ng1 : number of goals remaining at the current level (before cmd)
-     ngl1 : stack of previous levels with their remaining goals
-     ng : number of goals after the execution of cmd
-     beginend : special indentation stack for { } *)
-  let ngprev = List.fold_left (+) ng1 ngl1 in
-  let new_ngl =
-    if ng > ngprev then
-      (* We've branched *)
-      (ng - ngprev + 1, ng1 - 1 :: ngl1)
-    else if ng < ngprev then
-      (* A subgoal have been solved. Let's compute the new current level
-	 by discarding all levels with 0 remaining goals. *)
-      let rec loop = function
-	| (0, ng2::ngl2) -> loop (ng2,ngl2)
-	| p -> p
-      in loop (ng1-1, ngl1)
-    else
-      (* Standard case, same goal number as before *)
-      (ng1, ngl1)
-  in
-  (* When a subgoal have been solved, separate this block by an empty line *)
-  let new_nl = (ng < ngprev)
-  in
-  (* Indentation depth *)
-  let ind = List.length ngl1
-  in
-  (* Some special handling of bullets and { }, to get a nicer display *)
-  let pred n = max 0 (n-1) in
-  let ind, nl, new_beginend = match cmd with
-    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
-    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
-    | VernacBullet _ -> pred ind, nl, beginend
-    | _ -> ind, nl, beginend
-  in
-  let pp =
-    (if nl then fnl () else mt ()) ++
-    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
-  in
-  (new_ngl, new_nl, new_beginend, pp :: ppl)
-
-let show_script ?proof () =
-  try
-    let prf =
-      try match proof with
-      | None -> Some (Pfedit.get_current_proof_name ())
-      | Some (p,_) -> Some (p.Proof_global.id)
-      with Proof_global.NoCurrentProof -> None
-    in
-    let cmds = get_script prf in
-    let _,_,_,indented_cmds =
-      List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
-    in
-    let indented_cmds = List.rev (indented_cmds) in
-    msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
-  with Vcs_aux.Expired -> ()
+let get_all_proof_names ~doc =
+  List.map unmangle (CList.map_filter proofname (VCS.branches ()))
 
 (* Export hooks *)
 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
+let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+
+type document = VCS.vcs
+let backup () = VCS.backup ()
+let restore d = VCS.restore d
+
+
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index b8a2a385..35ce77a3 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -1,36 +1,120 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
-open Vernacexpr
 open Names
-open Feedback
-open Loc
 
 (** state-transaction-machine interface *)
 
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]
-   having edit id [eid].  [check] is called on the AST.
-   The [ontop] parameter is just for asserting the GUI is on sync, but
-   will eventually call edit_at on the fly if needed.
-   The sentence [s] is parsed in the state [ontop].
-   If [newtip] is provided, then the returned state id is guaranteed to be
-   [newtip] *)
-val add :
-  ontop:Stateid.t -> ?newtip:Stateid.t ->
-  ?check:(vernac_expr located -> unit) ->
-  bool -> edit_id -> string ->
-    Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
-
-(* parses and executes a command at a given state, throws away its side effects
-   but for the printings.  Feedback is sent with report_with (defaults to dummy
-   state id)  *)
-val query :
-  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
+(* Flags *)
+module AsyncOpts : sig
+
+  type cache = Force
+  type async_proofs = APoff | APonLazy | APon
+  type tac_error_filter = [ `None | `Only of string list | `All ]
+
+  type stm_opt = {
+    async_proofs_n_workers : int;
+    async_proofs_n_tacworkers : int;
+
+    async_proofs_cache : cache option;
+    async_proofs_mode : async_proofs;
+
+    async_proofs_private_flags : string option;
+    async_proofs_full : bool;
+    async_proofs_never_reopen_branch : bool;
+
+    async_proofs_tac_error_resilience : tac_error_filter;
+    async_proofs_cmd_error_resilience : bool;
+    async_proofs_delegation_threshold : float;
+  }
+
+  val default_opts : stm_opt
+
+end
+
+(** The STM document type [stm_doc_type] determines some properties
+   such as what uncompleted proofs are allowed and what gets recorded
+   to aux files. *)
+type stm_doc_type =
+  | VoDoc       of string       (* file path *)
+  | VioDoc      of string       (* file path *)
+  | Interactive of DirPath.t    (* module path *)
+
+(** Coq initalization options:
+
+ - [doc_type]: Type of document being created.
+
+ - [require_libs]: list of libraries/modules to be pre-loaded at
+   startup. A tuple [(modname,modfrom,import)] is equivalent to [From
+   modfrom Require modname]; [import] works similarly to
+   [Library.require_library_from_dirpath], [Some false] will import
+   the module, [Some true] will additionally export it.
+
+*)
+type stm_init_options = {
+  (* The STM will set some internal flags differently depending on the
+     specified [doc_type]. This distinction should dissappear at some
+     some point. *)
+  doc_type     : stm_doc_type;
+
+  (* Initial load path in scope for the document. Usually extracted
+     from -R options / _CoqProject *)
+  iload_path   : Mltop.coq_path list;
+
+  (* Require [require_libs] before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  require_libs : (string * string option * bool option) list;
+
+  (* STM options that apply to the current document. *)
+  stm_options  : AsyncOpts.stm_opt;
+}
+(* fb_handler   : Feedback.feedback -> unit; *)
+
+(** The type of a STM document *)
+type doc
+
+(** [init_core] performs some low-level initalization; should go away
+   in future releases. *)
+val init_core : unit -> unit
+
+(** [new_doc opt] Creates a new document with options [opt] *)
+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 ->
+  Vernacexpr.vernac_control CAst.t
+
+(* Reminder: A parsable [pa] is constructed using
+   [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
+
+exception End_of_input
+
+(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
+   the state [ontop].
+   The [ontop] parameter just asserts that the GUI is on
+   sync, but it will eventually call edit_at on the fly if needed.
+   If [newtip] is provided, then the returned state id is guaranteed
+   to be [newtip] *)
+val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
+  bool -> Vernacexpr.vernac_control CAst.t ->
+  doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* [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
 
 (* [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
@@ -42,24 +126,28 @@ val query :
    If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
 *)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
-val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
+val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
+
+(* [observe doc sid]] Check / execute span [sid] *)
+val observe : doc:doc -> Stateid.t -> doc
 
-(* Evaluates the tip of the current branch *)
-val finish : unit -> unit
+(* [finish doc] Fully checks a document up to the "current" tip. *)
+val finish : doc:doc -> doc
 
-val observe : Stateid.t -> unit
+(* Internal use (fake_ide) only, do not use *)
+val wait : doc:doc -> doc
 
 val stop_worker : string -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
-val join : unit -> unit
+val join : doc:doc -> doc
 
 (* Saves on the disk a .vio corresponding to the current status:
    - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
      of the completed tasks is a failure) *)
-val snapshot_vio : DirPath.t -> string -> unit
+val snapshot_vio : doc:doc -> DirPath.t -> string -> doc
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
  * after having built a .vio in batch mode *)
@@ -74,23 +162,17 @@ val finish_tasks : string ->
     tasks -> Library.seg_univ * Library.seg_proofs
 
 (* Id of the tip of the current branch *)
-val get_current_state : unit -> Stateid.t
-
-(* Misc *)
-val init : unit -> unit
+val get_current_state : doc:doc -> Stateid.t
+val get_ldir : doc:doc -> Names.DirPath.t
 
 (* This returns the node at that position *)
-val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
+val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
 
 (* Reorders the task queue putting forward what is in the perspective *)
-val set_perspective : Stateid.t list -> unit
-
-type document
-val backup : unit -> document
-val restore : document -> unit
+val set_perspective : doc:doc -> Stateid.t list -> unit
 
 (** workers **************************************************************** **)
 
@@ -105,20 +187,20 @@ module QueryTask : AsyncTaskQueue.Task
    While checking a proof, if an error occurs in a (valid) block then
    processing can skip the entire block and go on to give feedback
    on the rest of the proof.
-  
+
    static_block_detection and dynamic_block_validation are run when
    the closing block marker is parsed/executed respectively.
-  
+
    static_block_detection is for example called when "}" is parsed and
    declares a block containing all proof steps between it and the matching
    "{".
-  
+
    dynamic_block_validation is called when an error "crosses" the "}" statement.
    Depending on the nature of the goal focused by "{" the block may absorb the
    error or not.  For example if the focused goal occurs in the type of
    another goal, then the block is leaky.
    Note that one can design proof commands that need no dynamic validation.
-  
+
    Example of document:
 
       .. { tac1. tac2. } ..
@@ -126,7 +208,7 @@ module QueryTask : AsyncTaskQueue.Task
    Corresponding DAG:
 
       .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
-                       
+
    Declaration of block  [-------------------------------------------]
 
       start = 5            the first state_id that could fail in the block
@@ -147,7 +229,7 @@ type static_block_declaration = {
 
 type document_node = {
   indentation : int;
-  ast : Vernacexpr.vernac_expr;
+  ast : Vernacexpr.vernac_control;
   id : Stateid.t;
 }
 
@@ -162,11 +244,11 @@ type static_block_detection =
 type recovery_action = {
   base_state : Stateid.t;
   goals_to_admit : Goal.goal list;
-  recovery_command : Vernacexpr.vernac_expr option;
+  recovery_command : Vernacexpr.vernac_control option;
 }
 
 type dynamic_block_error_recovery =
-  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+  doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
 
 val register_proof_block_delimiter :
   Vernacexpr.proof_block_name ->
@@ -182,43 +264,26 @@ val register_proof_block_delimiter :
  * the name of the Task(s) above) *)
 
 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
-(* called with true before and with false after a tactic explicitly
- * in the document is run *)
-val tactic_being_run_hook : (bool -> unit) Hook.t
 
 (* Messages from the workers to the master *)
 val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
 
-type state = {
-  system : States.state;
-  proof : Proof_global.state;
-  shallow : bool
-}
-val state_of_id :
-  Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
-
-(** read-eval-print loop compatible interface ****************************** **)
+val get_doc : Feedback.doc_id -> doc
 
-(* Adds a new line to the document.  It replaces the core of Vernac.interp.
-   [finish] is called as the last bit of this function if the system
-   is running interactively (-emacs or coqtop). *)
-val interp : bool -> vernac_expr located -> unit
+val state_of_id : doc:doc ->
+  Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
 
 (* Queries for backward compatibility *)
-val current_proof_depth : unit -> int
-val get_all_proof_names : unit -> Id.t list
-val get_current_proof_name : unit -> Id.t option
-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)
+val current_proof_depth : doc:doc -> int
+val get_all_proof_names : doc:doc -> Id.t list
+
+(** Enable STM debugging *)
+val stm_debug : bool ref
+
+type document
+val backup : unit -> document
+val restore : document -> unit
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 939ee187..72b53801 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -4,8 +4,8 @@ Vcs
 TQueue
 WorkerPool
 Vernac_classifier
-Lemmas
 CoqworkmgrApi
+WorkerLoop
 AsyncTaskQueue
 Stm
 ProofBlockDelimiter
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index a0b08778..33744e73 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 PriorityQueue : sig
@@ -88,7 +90,7 @@ let broadcast { lock = m; cond = c } =
 
 let push { queue = q; lock = m; cond = c; release } x =
   if release then CErrors.anomaly(Pp.str
-    "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
+    "TQueue.push while being destroyed! Only 1 producer/destroyer allowed.");
   Mutex.lock m;
   PriorityQueue.push q x;
   Condition.broadcast c;
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 27eca12a..e098c37f 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* Thread safe queue with some extras *)
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index d5333d10..3b91df86 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -1,18 +1,16 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)
+module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
-let () = Coqtop.toploop_run := W.main_loop
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
 
diff --git a/stm/vcs.ml b/stm/vcs.ml
index d3886464..4bd46286 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 open Pp
@@ -74,8 +76,6 @@ module Dag = Dag.Make(OT)
 
 type id = OT.t
 
-module NodeSet = Dag.NodeSet
-
 module Branch =
 struct
   type t = string
@@ -115,7 +115,7 @@ let add_node vcs id edges =
 
 let get_branch vcs head =
   try BranchMap.find head vcs.heads
-  with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
+  with Not_found -> anomaly (str"head " ++ str head ++ str" not found.")
 
 let reset_branch vcs head id =
   let map name h =
diff --git a/stm/vcs.mli b/stm/vcs.mli
index 46b40f8a..47622ef6 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* This module builds a VCS like interface on top of Dag, used to build
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index dc5be08a..f68c8b32 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -1,16 +1,20 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
-open Vernacexpr
 open CErrors
+open Util
 open Pp
+open CAst
+open Vernacexpr
 
-let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+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 ""
 
@@ -30,13 +34,8 @@ let string_of_vernac_type = function
       "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
-  | VtQuery (b,(id,route)) ->
-      "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
-      " route " ^ string_of_int route
-  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
-      "Stm " ^ string_of_in_script b
-  | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
-  | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+  | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+  | VtMeta -> "Meta "
 
 let string_of_vernac_when = function
   | VtLater -> "Later"
@@ -52,65 +51,26 @@ let declare_vernac_classifier
 =
   classifiers := !classifiers @ [s,f]
 
-let elide_part_of_script_and_now (a, _) =
-  match a with
-  | VtQuery (_,id) -> VtQuery (false,id), VtNow
-  | VtStm (x, _) -> VtStm (x, false), VtNow
-  | x -> x, VtNow
-
-let make_polymorphic (a, b as x) =
-  match a with
-  | VtStartProof (x, _, ids) ->
-      VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
-  | _ -> x
+let idents_of_name : Names.Name.t -> Names.Id.t list =
+  function
+  | Names.Anonymous -> []
+  | Names.Name n -> [n]
 
-let undo_classifier = ref (fun _ -> assert false)
-let set_undo_classifier f = undo_classifier := f
-
-let rec classify_vernac e =
-  let static_classifier e = match e with
-    (* PG compatibility *)
-    | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
-    | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
-      when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
+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 (["Universe"; "Polymorphism"],_)
-    | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
-    (* Stm *)
-    | VernacStm Finish -> VtStm (VtFinish, true), VtNow
-    | VernacStm Wait -> VtStm (VtWait, true), VtNow
-    | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
-    | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
-    | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
-    | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
-    | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
-    (* Nested vernac exprs *)
-    | VernacProgram e -> classify_vernac e
-    | VernacLocal (_,e) -> classify_vernac e
-    | VernacPolymorphic (b, e) -> 
-      if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
-	make_polymorphic (classify_vernac e)
-      else classify_vernac e
-    | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
-    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
-        (match classify_vernac e with
-        | ( VtQuery _ | VtProofStep _ | VtSideff _
-          | VtStm _ | VtProofMode _ ), _ as x -> x
-        | VtQed _, _ ->
-            VtProofStep { parallel = `No; proof_block_detection = None },
-            VtNow
-        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+    | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
+      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+       VtSideff [], VtNow
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
     | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
     | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ ->
-        VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+    | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
     (* ProofStep *)
     | VernacProof _ 
     | VernacFocus _ | VernacUnfocus
@@ -127,51 +87,59 @@ let rec classify_vernac e =
                       proof_block_detection = Some "curly" },
         VtLater
     (* Options changing parser *)
-    | VernacUnsetOption (["Default";"Proof";"Using"])
-    | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
+    | VernacUnsetOption (_, ["Default";"Proof";"Using"])
+    | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
-    | VernacDefinition (
-       (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
-        VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
-    | VernacDefinition (_,((_,i),_),ProveBody _) ->
-        VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
-    | VernacStartTheoremProof (_,l,_) ->
-        let ids = 
-          CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
-        VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
-    | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
-    | VernacFixpoint (_,l) ->
+    | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
+      VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+
+    | VernacDefinition (_,({v=i},_),ProveBody _) ->
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater
+    | VernacStartTheoremProof (_,l) ->
+        let ids = List.map (fun (({v=i}, _), _) -> i) l in
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+    | VernacFixpoint (discharge,l) ->
+       let guarantee =
+         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
+       in
         let ids, open_proof =
-          List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
+          List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+        then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
         else VtSideff ids, VtLater
-    | VernacCoFixpoint (_,l) ->
+    | VernacCoFixpoint (discharge,l) ->
+       let guarantee =
+         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
+       in
         let ids, open_proof =
-          List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
+          List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+        then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
-        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
-        VtSideff ids, VtLater    
-    | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
-    | VernacInductive (_,_,l) ->
-        let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
-        | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
-        | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
+        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
+        VtSideff ids, VtLater
+    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
+    | VernacInductive (_, _,_,l) ->
+        let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
+        | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
+        | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
-            | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n
+            | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n
             | _ -> None) l) l in
         VtSideff (List.flatten ids), VtLater
     | VernacScheme l ->
-        let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
+        let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
         VtSideff ids, VtLater
-    | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
-    | VernacBeginSection (_,id) -> VtSideff [id], VtLater
+    | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater
+    | VernacBeginSection {v=id} -> VtSideff [id], VtLater
     | VernacUniverse _ | VernacConstraint _
     | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
@@ -181,7 +149,7 @@ let rec classify_vernac e =
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _
+    | VernacUnsetOption _ | VernacSetOption _
     | VernacAddOption _ | VernacRemoveOption _
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _
@@ -195,43 +163,58 @@ let rec classify_vernac e =
     (* (Local) Notations have to disappear *)
     | VernacEndSegment _ -> VtSideff [], VtNow
     (* Modules with parameters have to be executed: can import notations *)
-    | VernacDeclareModule (exp,(_,id),bl,_)
-    | VernacDefineModule (exp,(_,id),bl,_,_) ->
+    | VernacDeclareModule (exp,{v=id},bl,_)
+    | VernacDefineModule (exp,{v=id},bl,_,_) ->
         VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
-    | VernacDeclareModuleType ((_,id),bl,_,_) ->
+    | VernacDeclareModuleType ({v=id},bl,_,_) ->
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
     | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
-    | VernacSyntaxExtension _ 
+    | VernacSyntaxExtension _
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
-    | VernacProofMode _ 
+    | VernacProofMode _ -> VtSideff [], VtNow
     (* These are ambiguous *)
     | VernacInstance _ -> VtUnknown, VtNow
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
+    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
-    | VernacWriteState _ -> VtUnknown, VtNow
-    | VernacError _ -> assert false
+    | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
-        with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
+        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
+      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 _
+          | VtProofMode _ | VtMeta), _ as x -> x
+        | VtQed _, _ ->
+            VtProofStep { parallel = `No; proof_block_detection = None },
+            VtNow
+        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
   in
-  let res = static_classifier e in
-    if Flags.is_universe_polymorphism () then
-      make_polymorphic res
-    else res
+  static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
 
-let classify_as_query =
-  VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+let classify_as_query = VtQuery (true,Feedback.default_route), 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 45ca5cf6..abbc04e8 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 open Vernacexpr
@@ -12,15 +14,12 @@ open Genarg
 val string_of_vernac_classification : vernac_classification -> string
 
 (** What does a vernacular do *)
-val classify_vernac : vernac_expr -> vernac_classification
+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
 
-(** Set by Stm *)
-val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
-
 (** Standard constant classifiers *)
 val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index a6237daa..64f19e1f 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 open Util
@@ -14,7 +16,7 @@ let check_vio (ts,f) =
   Stm.set_compilation_hints long_f_dot_v;
   List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
 
-module Worker = Spawn.Sync(struct end)
+module Worker = Spawn.Sync ()
 
 module IntOT = struct
   type t = int
@@ -24,7 +26,7 @@ end
 module Pool = Map.Make(IntOT)
 
 let schedule_vio_checking j fs =
-  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
+  if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
@@ -98,7 +100,7 @@ let schedule_vio_checking j fs =
   exit !rc
 
 let schedule_vio_compilation j fs =
-  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
+  if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
@@ -107,7 +109,7 @@ let schedule_vio_compilation j fs =
     let long_f_dot_v = Loadpath.locate_file (f^".v") in
     let aux = Aux_file.load_aux_file_for long_f_dot_v in
     let eta =
-      try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
+      try float_of_string (Aux_file.get aux "vo_compile_time")
       with Not_found -> 0.0 in
     jobs := (f, eta) :: !jobs)
   fs;
diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli
index c0b6d9e6..177b3b2d 100644
--- a/stm/vio_checking.mli
+++ b/stm/vio_checking.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 (* [check_vio tasks file] checks the [tasks] stored in [file] *)
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
new file mode 100644
index 00000000..5445925b
--- /dev/null
+++ b/stm/workerLoop.ml
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   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
new file mode 100644
index 00000000..f02edb9b
--- /dev/null
+++ b/stm/workerLoop.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*         *   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
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 9623765d..0ff66686 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 type worker_id = string
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index 75c32536..0f1237b5 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 type worker_id = string