Adding a stm/ folder, as asked during last workgroup. It was essentially moving

files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.

19 files changed, 3790 insertions, 0 deletions

diff --git a/stm/dag.ml b/stm/dag.ml
new file mode 100644
index 000000000..9622f4c1f
--- /dev/null
+++ b/stm/dag.ml
@@ -0,0 +1,134 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type S = sig
+
+  module Cluster :
+  sig
+    type 'd t
+    val equal : 'd t -> 'd t -> bool
+    val compare : 'd t -> 'd t -> int
+    val to_string : 'd t -> string
+    val data : 'd t -> 'd
+  end
+
+  type node
+  module NodeSet : Set.S with type elt = node
+
+  type ('edge,'info,'cdata) t
+
+  val empty : ('e,'i,'d) t
+
+  val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t
+  val from_node : ('e,'i,'d) t -> node -> (node * 'e) list
+  val mem : ('e,'i,'d) t -> node -> bool
+  val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t
+  val del_nodes : ('e,'i,'d) t -> NodeSet.t  -> ('e,'i,'d) t
+  val all_nodes : ('e,'i,'d) t -> NodeSet.t
+
+  val iter : ('e,'i,'d) t ->
+    (node -> 'd Cluster.t option -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
+  val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
+  val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
+
+  val get_info : ('e,'i,'d) t -> node -> 'i option
+  val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
+  val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
+
+end
+
+module Make(OT : Map.OrderedType) = struct
+
+module Cluster =
+struct
+  type 'd t = 'd * int
+  let equal (_,i1) (_,i2) = Int.equal i1 i2
+  let compare (_,i1) (_,i2) = Int.compare i1 i2
+  let to_string (_,i) = string_of_int i
+  let data (d,_) = d
+end
+
+type node = OT.t
+
+module NodeMap = CMap.Make(OT)
+module NodeSet = Set.Make(OT)
+
+type ('edge,'info,'data) t = {
+  graph : (node * 'edge) list NodeMap.t;
+  clusters : 'data Cluster.t NodeMap.t;
+  infos : 'info NodeMap.t;
+}
+
+let empty = {
+  graph = NodeMap.empty;
+  clusters = NodeMap.empty;
+  infos = NodeMap.empty;
+}
+
+let mem { graph } id = NodeMap.mem id graph
+
+let add_edge dag from trans dest = { dag with
+  graph =
+    try NodeMap.modify from (fun _ arcs -> (dest, trans) :: arcs) dag.graph
+    with Not_found -> NodeMap.add from [dest, trans] dag.graph }
+
+let from_node { graph } id = NodeMap.find id graph
+
+let del_edge dag id tgt = { dag with
+  graph =
+    try
+      let modify _ arcs =
+        let filter (d, _) = OT.compare d tgt <> 0 in
+        List.filter filter arcs
+      in
+      NodeMap.modify id modify dag.graph
+    with Not_found -> dag.graph }
+
+let del_nodes dag s = {
+  infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos;
+  clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters;
+  graph = NodeMap.filter (fun n l ->
+      let drop = NodeSet.mem n s in
+      if not drop then
+        assert(List.for_all (fun (n',_) -> not(NodeSet.mem n' s)) l);
+      not drop)
+    dag.graph }
+
+let clid = ref 1
+let create_cluster dag l data =
+  incr clid;
+  { dag with clusters =
+     List.fold_right (fun x clusters ->
+       NodeMap.add x (data, !clid) clusters) l dag.clusters }
+
+let cluster_of dag id =
+  try Some (NodeMap.find id dag.clusters)
+  with Not_found -> None
+
+let del_cluster dag c =
+  { dag with clusters =
+     NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters }
+
+let get_info dag id =
+  try Some (NodeMap.find id dag.infos)
+  with Not_found -> None
+
+let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos }
+
+let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos }
+
+let iter dag f =
+  NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph
+
+let all_nodes dag = NodeMap.domain dag.graph
+
+end
+
diff --git a/stm/dag.mli b/stm/dag.mli
new file mode 100644
index 000000000..702ccd80f
--- /dev/null
+++ b/stm/dag.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type S = sig
+
+  (* A cluster is just a set of nodes.  This set holds some data.
+     Stm uses this to group nodes contribution to the same proofs and
+     that can be evaluated asynchronously *)
+  module Cluster :
+  sig
+    type 'd t
+    val equal : 'd t -> 'd t -> bool
+    val compare : 'd t -> 'd t -> int
+    val to_string : 'd t -> string
+    val data : 'd t -> 'd
+  end
+
+  type node
+  module NodeSet : Set.S with type elt = node
+
+  type ('edge,'info,'cdata) t
+  
+  val empty : ('e,'i,'d) t
+
+  val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t
+  val from_node : ('e,'i,'d) t -> node -> (node * 'e) list
+  val mem : ('e,'i,'d) t -> node -> bool
+  val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t
+  val del_nodes : ('e,'i,'d) t -> NodeSet.t  -> ('e,'i,'d) t
+  val all_nodes : ('e,'i,'d) t -> NodeSet.t
+
+  val iter : ('e,'i,'d) t -> 
+    (node -> 'd Cluster.t option -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
+  val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
+  val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
+
+  val get_info : ('e,'i,'d) t -> node -> 'i option
+  val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
+  val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
+
+end
+
+module Make(OT : Map.OrderedType) : S with type node = OT.t
+
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
new file mode 100644
index 000000000..8f16ad5a4
--- /dev/null
+++ b/stm/lemmas.ml
@@ -0,0 +1,431 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \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 Errors
+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
+
+(* Support for mutually proved theorems *)
+
+let retrieve_first_recthm = function
+  | VarRef id ->
+      (pi2 (Global.lookup_named id),variable_opacity id)
+  | ConstRef cst ->
+      let cb = Global.lookup_constant cst in
+      (body_of_constant 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, 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 indexes =
+	        search_guard Loc.ghost env
+                  possible_indexes fixdecls in
+              mkFix ((indexes,0),fixdecls),  eff
+          | _ -> body, 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) when
+              let mind = Global.lookup_mind kn in
+              mind.mind_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_betadeltaiota_stack env Evd.empty c))
+        (Global.env()) hyps in
+      let ind_hyps =
+        List.flatten (List.map_i (fun i (_,b,t) ->
+          match kind_of_term t with
+          | Ind (kn,_ as ind) when
+                let mind = Global.lookup_mind kn in
+                mind.mind_finite && Option.is_empty b ->
+              [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_betadeltaiota_stack cclenv Evd.empty ccl in
+        match kind_of_term whnf_ccl with
+        | Ind (kn,_ as ind) when
+              let mind = Global.lookup_mind kn in
+              Int.equal mind.mind_ntypes n && not mind.mind_finite ->
+            [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 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 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 id const do_guard (locality,kind) hook =
+  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 id ~local (DefinitionEntry const, k) in
+	(locality, ConstRef kn) in
+  definition_message id;
+  hook l r
+
+let default_thm_id = Id.of_string "Unnamed_thm"
+
+let compute_proof_name locality = function
+  | Some (loc,id) ->
+      (* 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
+  | None ->
+      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
+
+let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
+  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,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 decl = (ParameterEntry (None,t_i,None), k) in
+          let kn = declare_constant id ~local decl in
+          (locality,ConstRef kn,imps))
+  | Some body ->
+      let k = Kindops.logical_kind_of_goal_kind kind in
+      let body_i = match kind_of_term body with
+        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+        | CoFix (0,decls) -> mkCoFix (i,decls)
+        | _ -> anomaly (Pp.str "Not a proof by induction") in
+      match locality with
+      | Discharge ->
+          let const = { const_entry_body =
+                Future.from_val (body_i,Declareops.no_seff);
+              const_entry_secctx = None;
+              const_entry_type = Some t_i;
+              const_entry_opaque = opaq;
+              const_entry_inline_code = false;
+              const_entry_feedback = None;
+          } in
+	  let c = SectionLocalDef const in
+	  let _ = declare_variable id (Lib.cwd(), c, k) in
+          (Discharge,VarRef id,imps)
+      | Local | Global ->
+        let local = match locality with
+        | Local -> true
+        | Global -> false
+        | Discharge -> assert false
+        in
+        let const = { const_entry_body =
+              Future.from_val (body_i,Declareops.no_seff);
+            const_entry_secctx = None;
+            const_entry_type = Some t_i;
+            const_entry_opaque = opaq;
+            const_entry_inline_code = false;
+            const_entry_feedback = None;
+        } 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 proof =
+  let id,const,do_guard,persistence,hook = proof in
+  save id const 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 proof save_ident =
+  let id,const,do_guard,persistence,hook = proof in
+  check_anonymity id save_ident;
+  save save_ident const do_guard persistence hook
+
+let save_anonymous_with_strength proof kind save_ident =
+  let id,const,do_guard,_,hook = proof in
+  check_anonymity id save_ident;
+  (* we consider that non opaque behaves as local for discharge *)
+  save save_ident const do_guard (Global, Proof kind) hook
+
+(* Admitted *)
+
+let admit hook () =
+  let (id,k,typ) = Pfedit.current_proof_statement () in
+  let e = Pfedit.get_used_variables(), typ, None in
+  let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
+  let () = match fst k with
+  | Global -> ()
+  | Local | Discharge ->
+    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+      str "declared as an axiom.")
+  in
+  let () = assumption_message id in
+  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,persistence)) =
+    Pfedit.cook_this_proof proof
+  in
+  id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
+
+let standard_proof_terminator compute_guard hook =
+  let open Proof_global in function
+  | Admitted ->
+      admit hook ();
+      Pp.feedback Interface.AddedAxiom
+  | Proved (is_opaque,idopt,proof) ->
+      let proof = get_proof proof compute_guard hook is_opaque in
+      begin match idopt with
+      | None -> save_named proof
+      | Some ((_,id),None) -> save_anonymous proof id
+      | Some ((_,id),Some kind) -> 
+          save_anonymous_with_strength proof kind id
+      end
+
+let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = standard_proof_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 kind 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 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 = Proofview.V82.tactic (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,(t,(_,imps)))::other_thms ->
+      let hook strength ref =
+        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
+            List.map_i (save_remaining_recthms kind 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;
+	  hook strength ref) thms_data in
+      start_proof id kind t ?init_tac hook ~compute_guard:guard
+
+let start_proof_com kind thms hook =
+  let evdref = ref Evd.empty in
+  let env0 = Global.env () in
+  let thms = List.map (fun (sopt,(bl,t,guard)) ->
+    let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
+    let t', imps' = interp_type_evars_impls ~impls evdref env t in
+    check_evars_are_solved env Evd.empty !evdref;
+    let ids = List.map pi1 ctx in
+      (compute_proof_name (fst 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
+  start_proof_with_initialization kind recguard thms snl hook
+
+
+(* Saving a proof *)
+
+let save_proof ?proof = function
+  | Vernacexpr.Admitted ->
+      Proof_global.get_terminator() Proof_global.Admitted
+  | Vernacexpr.Proved (is_opaque,idopt) ->
+      let (proof_obj,terminator) =
+        match proof with
+        | None -> Proof_global.close_proof (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 ();
+      terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
+
+(* Miscellaneous *)
+
+let get_current_context () =
+  try Pfedit.get_current_goal_context ()
+  with e when Logic.catchable_exception e ->
+    (Evd.empty, Global.env())
+
+
+
+
+
+
+
+
+
+
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
new file mode 100644
index 000000000..bbe383a85
--- /dev/null
+++ b/stm/lemmas.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \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 Constrexpr
+open Tacexpr
+open Vernacexpr
+open Pfedit
+
+(** 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 -> goal_kind -> ?sign:Environ.named_context_val -> types ->
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+   unit declaration_hook -> unit
+
+val start_proof_com : goal_kind ->
+  (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+  unit declaration_hook -> unit
+
+val start_proof_with_initialization : 
+  goal_kind -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
+  -> int list option -> unit declaration_hook -> unit
+
+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/spawned.ml b/stm/spawned.ml
new file mode 100644
index 000000000..d02594569
--- /dev/null
+++ b/stm/spawned.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Spawn
+
+let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
+let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+
+type chandescr = AnonPipe | Socket of string * int
+
+let handshake cin cout =
+  try
+    match input_value cin with
+    | Hello(v, pid) when v = proto_version ->
+        prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
+        output_value cout (Hello (proto_version,Unix.getpid ())); flush cout
+    | _ -> raise (Failure "handshake protocol")
+  with
+  | Failure s | Invalid_argument s | Sys_error s ->
+      pr_err ("Handshake failed: "  ^ s); raise (Failure "handshake")
+  | End_of_file ->
+      pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
+
+let open_bin_connection h p =
+  let open Unix in
+  let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in
+  set_binary_mode_in cin true;
+  set_binary_mode_out cout true;
+  cin, cout
+
+let controller h p =
+  prerr_endline "starting controller thread";
+  let main () =
+    let ic, oc = open_bin_connection h p in
+    let rec loop () =
+      try
+        match input_value ic with
+        | Hello _ -> prerr_endline "internal protocol error"; exit 1
+        | ReqDie -> prerr_endline "death sentence received"; exit 0
+        | ReqStats ->
+            output_value oc (RespStats (Gc.stat ())); flush oc; loop ()
+      with
+      | e ->
+        prerr_endline ("control channel broken: " ^ Printexc.to_string e);
+        exit 1 in
+    loop () in
+  ignore(Thread.create main ())
+
+let main_channel = ref None
+let control_channel = ref None
+
+let channels = ref None
+
+let init_channels () =
+  if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
+  let () = match !main_channel with
+  | None -> ()
+  | Some (Socket(mh,mp)) ->
+    channels := Some (open_bin_connection mh mp);
+  | Some AnonPipe ->
+    let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
+    let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
+    Unix.dup2 Unix.stderr Unix.stdout;
+    set_binary_mode_in stdin true;
+    set_binary_mode_out stdout true;
+    channels := Some (stdin, stdout);
+  in
+  match !control_channel with
+  | None -> ()
+  | Some (Socket (ch, cp)) ->
+    controller ch cp
+  | Some AnonPipe ->
+    Errors.anomaly (Pp.str "control channel cannot be a pipe")
+
+let get_channels () =
+  match !channels with
+  | None -> Errors.anomaly(Pp.str "init_channels not called")
+  | Some(ic, oc) -> ic, oc
+
diff --git a/stm/spawned.mli b/stm/spawned.mli
new file mode 100644
index 000000000..18b88dc64
--- /dev/null
+++ b/stm/spawned.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* To link this file, threads are needed *)
+
+type chandescr = AnonPipe | Socket of string * int
+
+(* Argument parsing should set these *)
+val main_channel : chandescr option ref
+val control_channel : chandescr option ref
+
+(* Immediately after argument parsing one *must* call this *)
+val init_channels : unit -> unit
+
+(* Once initialized, these are the channels to talk with our master *)
+val get_channels : unit -> in_channel * out_channel
+
diff --git a/stm/stm.ml b/stm/stm.ml
new file mode 100644
index 000000000..e791e37cf
--- /dev/null
+++ b/stm/stm.ml
@@ -0,0 +1,2075 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+let process_id () =
+  match !Flags.async_proofs_mode with
+  | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 ->
+      "master" ^ string_of_int (Thread.id (Thread.self ()))
+  | Flags.APonParallel n -> "worker" ^ string_of_int n 
+
+let pr_err s = Printf.eprintf "%s] %s\n" (process_id ()) s; flush stderr
+
+let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+
+let (f_process_error, process_error_hook) = Hook.make ()
+let ((f_interp : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
+  Loc.t * Vernacexpr.vernac_expr -> unit) Hook.value), interp_hook) = Hook.make ()
+
+open Vernacexpr
+open Errors
+open Pp
+open Names
+open Util
+open Ppvernac
+open Vernac_classifier
+
+(* 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 fallback_to_lazy_if_marshal_error = ref true
+let fallback_to_lazy_if_slave_dies = ref true
+let async_proofs_workers_extra_env = ref [||]
+
+type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
+let pr_ast { expr } = pr_vernac expr
+
+(* Wrapper for Vernacentries.interp to set the feedback id *)
+let vernac_interp ?proof id { verbose; loc; expr } =
+  let internal_command = function
+    | VernacResetName _ | VernacResetInitial | VernacBack _
+    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in
+  if internal_command expr then begin
+    prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
+  end else begin
+    Pp.set_id_for_feedback (Interface.State id);
+    Aux_file.record_in_aux_set_at loc;
+    prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
+    let interp = Hook.get f_interp in
+    try interp ~verbosely:verbose ?proof (loc, expr)
+    with e ->
+      let e = Errors.push e in
+      raise (Hook.get f_process_error e)
+  end
+
+(* Wrapper for Vernac.parse_sentence to set the feedback id *)
+let vernac_parse eid s =
+  set_id_for_feedback (Interface.Edit eid);
+  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  Flags.with_option Flags.we_are_parsing (fun () ->
+    match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+    | None -> raise (Invalid_argument "vernac_parse")
+    | Some ast -> ast)
+  ()
+
+module Vcs_ = Vcs.Make(Stateid)
+type future_proof = Entries.proof_output list Future.computation
+type proof_mode = string
+type depth = int
+type cancel_switch = bool ref
+type branch_type =
+  [ `Master
+  | `Proof of proof_mode * depth
+  | `Edit of proof_mode * Stateid.t * Stateid.t ]
+type cmd_t = ast * Id.t list
+type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+type qed_t = {
+  qast : ast;
+  keep : vernac_qed_type;
+  mutable fproof : (future_proof * cancel_switch) option;
+  brname : Vcs_.Branch.t;
+  brinfo : branch_type Vcs_.branch_info
+}
+type seff_t = ast option
+type alias_t = Stateid.t
+type transaction =
+  | Cmd    of cmd_t
+  | Fork   of fork_t
+  | Qed    of qed_t
+  | Sideff of seff_t
+  | Alias  of alias_t
+  | Noop
+type step =
+  [ `Cmd    of cmd_t
+  | `Fork   of fork_t
+  | `Qed    of qed_t * Stateid.t
+  | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ]
+  | `Alias  of alias_t ]
+type visit = { step : step; next : Stateid.t }
+
+type state = {
+  system : States.state;
+  proof : Proof_global.state;
+  shallow : bool
+}
+type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
+type backup = { mine : branch; others : branch list }
+type 'vcs state_info = { (* Make private *)
+  mutable n_reached : int;
+  mutable n_goals : int;
+  mutable state : state option;
+  mutable vcs_backup : 'vcs option * backup option;
+}
+let default_info () =
+  { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None }
+
+(* Functions that work on a Vcs with a specific branch type *)
+module Vcs_aux : sig
+
+  val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int
+  val find_proof_at_depth :
+    (branch_type, 't, 'i) Vcs_.t -> int ->
+      Vcs_.Branch.t * branch_type Vcs_.branch_info
+  exception Expired
+  val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
+
+end = struct (* {{{ *)
+
+  let proof_nesting vcs =
+    List.fold_left max 0
+      (List.map_filter
+        (function
+         | { Vcs_.kind = `Proof (_,n) } -> Some n
+         | { Vcs_.kind = `Edit _ } -> Some 1
+         | _ -> None)
+        (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs)))
+
+  let find_proof_at_depth vcs pl =
+    try List.find (function
+          | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
+          | _, { Vcs_.kind = `Edit _ } -> anomaly(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"
+
+  exception Expired
+  let visit vcs id =
+    if Stateid.equal id Stateid.initial then
+      anomaly(str"Visiting the initial state id")
+    else if Stateid.equal id Stateid.dummy then
+      anomaly(str"Visiting the dummy state id")
+    else
+    try
+      match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
+      | [n, Cmd x] -> { step = `Cmd x; next = n }
+      | [n, Alias x] -> { step = `Alias x; next = n }
+      | [n, Fork x] -> { step = `Fork x; 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 (str ("Malformed VCS at node "^Stateid.to_string id))
+    with Not_found -> raise Expired
+
+end (* }}} *)
+
+(* Imperative wrap around VCS to obtain _the_ VCS *)
+module VCS : sig
+
+  exception Expired
+
+  module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t)
+  type id = Stateid.t
+  type 'branch_type branch_info = 'branch_type Vcs_.branch_info = {
+    kind : [> `Master] as 'branch_type;
+    root : id;
+    pos  : id;
+  }
+
+  type vcs = (branch_type, transaction, vcs state_info) Vcs_.t
+
+  val init : id -> unit
+
+  val current_branch : unit -> Branch.t
+  val checkout : Branch.t -> unit
+  val branches : unit -> Branch.t list
+  val get_branch : Branch.t -> branch_type branch_info
+  val get_branch_pos : Branch.t -> id
+  val new_node : unit -> id
+  val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
+  val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
+  val delete_branch : Branch.t -> unit
+  val commit : id -> transaction -> unit
+  val mk_branch_name : ast -> Branch.t
+  val edit_branch : Branch.t
+  val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit
+  val reset_branch : Branch.t -> id -> unit
+  val reachable : id -> Vcs_.NodeSet.t
+  val cur_tip : unit -> id
+
+  val get_info : id -> vcs state_info
+  val reached : id -> bool -> unit
+  val goals : id -> int -> unit
+  val set_state : id -> state -> unit
+  val get_state : id -> state option
+  val forget_state : id -> unit
+
+  (* cuts from start -> stop, raising Expired if some nodes are not there *)
+  val slice : start:id -> stop:id -> vcs
+  
+  val create_cluster : id list -> tip:id -> unit
+  val cluster_of : id -> id option
+  val delete_cluster_of : id -> unit
+
+  val proof_nesting : unit -> int
+  val checkout_shallowest_proof_branch : unit -> unit
+  val propagate_sideff : ast option -> unit
+
+  val gc : unit -> unit
+
+  val visit : id -> visit
+
+  val print : ?now:bool -> unit -> unit
+
+  val backup : unit -> vcs
+  val restore : vcs -> unit
+
+end = struct (* {{{ *)
+
+  include Vcs_
+  exception Expired = Vcs_aux.Expired
+
+  module StateidSet = Set.Make(Stateid)
+  open Printf
+
+  let print_dag vcs () = (* {{{ *)
+    let fname = "stm_" ^ process_id () in
+    let string_of_transaction = function
+      | Cmd (t, _) | Fork (t, _,_,_) ->
+          (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+      | Sideff (Some t) ->
+          sprintf "Sideff(%s)"
+            (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+      | Sideff None -> "EnvChange"
+      | Noop -> " "
+      | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id)
+      | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
+    let is_green id = 
+      match get_info vcs id with
+      | Some { state = Some _ } -> true
+      | _ -> false in
+    let is_red id =
+      match get_info vcs id with
+      | Some s -> Int.equal s.n_reached ~-1
+      | _ -> false in
+    let head = current_branch vcs in
+    let heads =
+      List.map (fun x -> x, (get_branch vcs x).pos) (branches vcs) in
+    let graph = dag vcs in
+    let quote s =
+      Str.global_replace (Str.regexp "\n") "<BR/>"
+       (Str.global_replace (Str.regexp "<") "&lt;"
+        (Str.global_replace (Str.regexp ">") "&gt;"
+         (Str.global_replace (Str.regexp "\"") "&quot;"
+          (Str.global_replace (Str.regexp "&") "&amp;"
+           (String.sub s 0 (min (String.length s) 20)))))) in
+    let fname_dot, fname_ps =
+      let f = "/tmp/" ^ Filename.basename fname in
+      f ^ ".dot", f ^ ".pdf" in
+    let node id = "s" ^ Stateid.to_string id in
+    let edge tr =
+      sprintf "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>"
+        (quote (string_of_transaction tr)) in
+    let ids = ref StateidSet.empty in
+    let clus = Hashtbl.create 13 in
+    let node_info id =
+      match get_info vcs id with
+      | None -> ""
+      | Some info ->
+          sprintf "<<FONT POINT-SIZE=\"12\">%s</FONT>" (Stateid.to_string id) ^
+          sprintf " <FONT POINT-SIZE=\"11\">r:%d g:%d</FONT>>"
+            info.n_reached info.n_goals in
+    let color id =
+      if is_red id then "red" else if is_green id then "green" else "white" in
+    let nodefmt oc id =
+      fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n"
+        (node id) (node_info id) (color id) in
+    let add_to_clus_or_ids from cf =
+      match cf with
+      | None -> ids := StateidSet.add from !ids; false
+      | Some c -> Hashtbl.replace clus c
+         (try let n = Hashtbl.find clus c in from::n
+         with Not_found -> [from]); true in
+    let oc = open_out fname_dot in
+    output_string oc "digraph states {\nsplines=ortho\n";
+    Dag.iter graph (fun from cf _ l ->
+      let c1 = add_to_clus_or_ids from cf in
+      List.iter (fun (dest, trans) ->
+       let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in
+       fprintf oc "%s -> %s [label=%s,labelfloat=%b];\n"
+           (node from) (node dest) (edge trans) (c1 && c2)) l
+    );
+    StateidSet.iter (nodefmt oc) !ids;
+    Hashtbl.iter (fun c nodes ->
+       fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c);
+       List.iter (nodefmt oc) nodes;
+       fprintf oc "color=blue; }\n"
+    ) clus;
+    List.iteri (fun i (b,id) ->
+      let shape = if Branch.equal head b then "box3d" else "box" in
+      fprintf oc "b%d -> %s;\n" i (node id);
+      fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
+        (Branch.to_string b);
+    ) heads;
+    output_string oc "}\n";
+    close_out oc;
+    ignore(Sys.command
+      ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
+  (* }}} *)
+  
+  type vcs = (branch_type, transaction, vcs state_info) t
+  let vcs : vcs ref = ref (empty Stateid.dummy)
+
+  let init id =
+    vcs := empty id;
+    vcs := set_info !vcs id (default_info ())
+
+  let current_branch () = current_branch !vcs
+
+  let checkout head = vcs := checkout !vcs head
+  let branches () = branches !vcs
+  let get_branch head = get_branch !vcs head
+  let get_branch_pos head = (get_branch head).pos
+  let new_node () =
+    let id = Stateid.fresh () in
+    vcs := set_info !vcs id (default_info ());
+    id
+  let merge id ~ours ?into branch =
+    vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
+  let delete_branch branch = vcs := delete_branch !vcs branch
+  let reset_branch branch id = vcs := reset_branch !vcs branch id
+  let commit id t = vcs := commit !vcs id t
+  let rewrite_merge id ~ours ~at branch =
+    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
+    | _ -> "branch")
+  let edit_branch = Branch.make "edit"
+  let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
+  let get_info id =
+    match get_info !vcs id with
+    | Some x -> x
+    | None -> raise Vcs_aux.Expired
+  let set_state id s = (get_info id).state <- Some s
+  let get_state id = (get_info id).state
+  let forget_state id = (get_info id).state <- None
+  let reached id b =
+    let info = get_info id in
+    if b then info.n_reached <- info.n_reached + 1
+    else info.n_reached <- -1
+  let goals id n = (get_info id).n_goals <- n
+  let cur_tip () = get_branch_pos (current_branch ())
+
+  let proof_nesting () = Vcs_aux.proof_nesting !vcs
+
+  let checkout_shallowest_proof_branch () =
+    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
+      | _ -> assert false
+    end else
+      let pl = proof_nesting () in
+      try
+        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 ("mode:" ^ mode);
+        Proof_global.activate_proof_mode mode
+      with Failure _ ->
+        checkout Branch.master;
+        Proof_global.disactivate_proof_mode "Classic"
+
+  (* copies the transaction on every open branch *)
+  let propagate_sideff t =
+    List.iter (fun b ->
+      checkout b;
+      let id = new_node () in
+      merge id ~ours:(Sideff t) ~into:b Branch.master)
+    (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
+  
+  let visit id = Vcs_aux.visit !vcs id
+
+  let slice ~start ~stop =
+    let l =
+      let rec aux id =
+        if Stateid.equal id stop then [] else
+        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 start ^
+                           " to "^Stateid.to_string stop))
+      in aux start in
+    let copy_info v id =
+      Vcs_.set_info v id
+        { (get_info id) with state = None; vcs_backup = None,None } in
+    let copy_info_w_state v id =
+      Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
+    let v = Vcs_.empty stop in
+    let v = copy_info v stop in
+    let v = List.fold_right (fun (id,tr) v ->
+      let v = Vcs_.commit v id tr in
+      let v = copy_info v id in
+      v) l v in
+    (* Stm should have reached the beginning of proof *)
+    assert (not (Option.is_empty (get_info stop).state));
+    (* We put in the new dag the most recent state known to master *)
+    let rec fill id =
+      if (get_info id).state = None then fill (Vcs_aux.visit v id).next
+      else copy_info_w_state v id in
+    fill start
+
+  let create_cluster l ~tip = vcs := create_cluster !vcs l tip
+  let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id)
+  let delete_cluster_of id =
+    Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id)
+
+  let gc () =
+    let old_vcs = !vcs in
+    let new_vcs, erased_nodes = gc old_vcs in
+    Vcs_.NodeSet.iter (fun id ->
+        match (Vcs_aux.visit old_vcs id).step with
+        | `Qed ({ fproof = Some (_, cancel_switch) }, _) ->
+             cancel_switch := true
+        | _ -> ())
+      erased_nodes;
+    vcs := new_vcs
+
+  module NB : sig (* Non blocking Sys.command *)
+
+    val command : now:bool -> (unit -> unit) -> unit
+
+  end = struct (* {{{ *)
+    
+    let m = Mutex.create ()
+    let c = Condition.create ()
+    let job = ref None
+    let worker = ref None
+
+    let set_last_job j =
+      Mutex.lock m;
+      job := Some j;
+      Condition.signal c;
+      Mutex.unlock m
+
+    let get_last_job () =
+      Mutex.lock m;
+      while Option.is_empty !job do Condition.wait c m; done;
+      match !job with
+      | None -> assert false
+      | Some x -> job := None; Mutex.unlock m; x
+
+    let run_command () =
+      try while true do get_last_job () () done
+      with e -> () (* No failure *)
+
+    let command ~now job =
+      if now then job ()
+      else begin
+        set_last_job job;
+        if Option.is_empty !worker then
+          worker := Some (Thread.create run_command ())
+      end
+
+  end (* }}} *)
+
+  let print ?(now=false) () =
+    if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs)
+
+  let backup () = !vcs
+  let restore v = vcs := v
+
+end (* }}} *)
+
+(* Fills in the nodes of the VCS *)
+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.
+      Warning: an optimization in installed_cached requires that state
+      modifying functions are always executed using this wrapper. *)
+  val define :
+    ?redefine:bool -> ?cache:Summary.marshallable -> (unit -> unit) -> Stateid.t -> unit
+
+  val install_cached : Stateid.t -> unit
+  val is_cached : Stateid.t -> bool
+
+
+  val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
+  (* to send states across worker/master *)
+  type frozen_state
+  val get_cached : Stateid.t -> frozen_state
+  val assign : Stateid.t -> frozen_state -> unit
+
+end = struct (* {{{ *)
+
+  (* cur_id holds Stateid.dummy in case the last attempt to define a state
+   * failed, so the global state may contain garbage *)
+  let cur_id = ref Stateid.dummy
+
+  (* 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 in_t, out_t = Dyn.create "state4future"
+  let () = Future.set_freeze
+    (fun () -> in_t (freeze_global_state `No, !cur_id))
+    (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
+
+  let is_cached id =
+    Stateid.equal id !cur_id ||
+    match VCS.get_info id with
+    | { state = Some _ } -> true
+    | _ -> false
+
+  let install_cached id =
+    if Stateid.equal id !cur_id then () else (* optimization *)
+    let s =
+      match VCS.get_info id with
+      | { state = Some s } -> s
+      | _ -> anomaly (str "unfreezing a non existing state") in
+    unfreeze_global_state s; cur_id := id
+
+  type frozen_state = state
+
+  let get_cached id =
+    try match VCS.get_info id with
+    | { state = Some s } -> s
+    | _ -> anomaly (str "not a cached state")
+    with VCS.Expired -> anomaly (str "not a cached state (expired)")
+
+  let assign id s =
+    try if VCS.get_state id = None then VCS.set_state id s
+    with VCS.Expired -> ()
+
+  let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+
+  let exn_on id ?valid e =
+    match Stateid.get e with
+    | Some _ -> e
+    | None ->
+        let loc = Option.default Loc.ghost (Loc.get_loc e) in
+        let msg = string_of_ppcmds (print e) in
+        Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg));
+        Stateid.add (Hook.get f_process_error e) ?valid id
+
+  let define ?(redefine=false) ?(cache=`No) f 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");
+    try
+      prerr_endline("defining "^str_id^" (cache="^
+        if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+      f ();
+      if cache = `Yes then freeze `No id
+      else if cache = `Shallow then freeze `Shallow id;
+      prerr_endline ("setting cur id to "^str_id);
+      cur_id := id;
+      feedback ~state_id:id Interface.Processed;
+      VCS.reached id true;
+      if Proof_global.there_are_pending_proofs () then
+        VCS.goals id (Proof_global.get_open_goals ());
+    with e ->
+      let e = Errors.push e in
+      let good_id = !cur_id in
+      cur_id := Stateid.dummy;
+      VCS.reached id false;
+      match Stateid.get e with
+      | Some _ -> raise e
+      | None -> raise (exn_on id ~valid:good_id e)
+
+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
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> Loc.ghost, id) ids in
+  SsExpr (SsSet ids)
+
+let get_hint_bp_time proof_name =
+  try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
+  with Not_found -> 1.0
+
+module Worker = Spawn.Sync(struct 
+  let add_timeout ~sec f =
+    ignore(Thread.create (fun () ->
+      while true do
+        Unix.sleep sec;
+        if not (f ()) then Thread.exit ()
+      done)
+    ())
+end)
+
+module WorkersPool = WorkerPool.Make(Worker)
+
+let record_pb_time proof_name loc time =
+  let proof_build_time = Printf.sprintf "%.3f" time in
+  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
+  end
+
+(* Slave processes (if initialized, otherwise local lazy evaluation) *)
+module Slaves : sig
+
+  (* (eventually) remote calls *)
+  val build_proof : loc:Loc.t ->
+    exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
+      name:string -> future_proof * 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
+
+  (* slave process main loop *)
+  val slave_main_loop : (unit -> unit) -> unit
+  val slave_init_stdout : unit -> unit
+
+  (* to disentangle modules *)
+  val set_reach_known_state :
+    (?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit
+
+  type tasks
+  val dump : (Future.UUID.t * int) list -> tasks
+  val check_task : string -> tasks -> int -> bool
+  val info_tasks : tasks -> (string * float * int) list
+  val finish_task :
+    string ->
+    Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    tasks -> int -> Library.seg_univ
+
+  val cancel_worker : int -> unit
+
+  val set_perspective : Stateid.t list -> unit
+
+end = struct (* {{{ *)
+
+
+  let cancel_worker n = WorkersPool.cancel (n-1)
+
+  let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
+  let set_reach_known_state f = reach_known_state := f
+
+  type 'a request =
+    ReqBuildProof of
+      (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * 'a * string
+
+  let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
+
+  type response =
+    | RespBuiltProof of Entries.proof_output list * float
+    | RespError of (* err, safe, msg, safe_states *)
+        Stateid.t * Stateid.t * std_ppcmds *
+          (Stateid.t * State.frozen_state) list
+    | RespFeedback of Interface.feedback
+    | RespGetCounterFreshLocalUniv
+    | RespGetCounterNewUnivLevel
+  let pr_response = function
+    | RespBuiltProof _ -> "Sucess"
+    | RespError _ -> "Error"
+    | RespFeedback { Interface.id = Interface.State id } ->
+        "Feedback on " ^ Stateid.to_string id
+    | RespFeedback _ -> assert false
+    | RespGetCounterFreshLocalUniv -> "GetCounterFreshLocalUniv"
+    | RespGetCounterNewUnivLevel -> "GetCounterNewUnivLevel"
+
+  type more_data =
+    | MoreDataLocalUniv of Univ.universe list
+    | MoreDataUnivLevel of Univ.universe_level list
+ 
+  type task =
+    | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
+        (Entries.proof_output list Future.assignement -> unit) * cancel_switch
+        * Loc.t * Future.UUID.t * string
+  let pr_task = function
+    | TaskBuildProof(_,bop,eop,_,_,_,_,s) ->
+        "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
+          ","^s^")"
+
+  let request_of_task task : Future.UUID.t request =
+    match task with
+    | TaskBuildProof (exn_info,bop,eop,_,_,loc,uuid,s) ->
+        ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,uuid,s)
+
+  let cancel_switch_of_task = function
+    | TaskBuildProof (_,_,_,_,c,_,_,_) -> c
+
+  let build_proof_here_core loc eop () =
+    let wall_clock1 = Unix.gettimeofday () in
+    if !Flags.batch_mode 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"
+      (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+    Proof_global.return_proof ()
+  let build_proof_here (id,valid) loc eop =
+    Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop)
+
+  let slave_respond msg =
+    match msg with
+    | ReqBuildProof(exn_info,eop,vcs,loc,_,_) ->
+        VCS.restore vcs;
+        VCS.print ();
+        let rc, time =
+          let wall_clock = Unix.gettimeofday () in
+          let l = Future.force (build_proof_here exn_info loc eop) in
+          List.iter (fun (_,se) -> Declareops.iter_side_effects (function
+            | Declarations.SEsubproof(_,
+               { Declarations.const_body = Declarations.OpaqueDef f } ) ->
+               Opaqueproof.join_opaque f
+            | _ -> ())
+          se) l;
+          l, Unix.gettimeofday () -. wall_clock in
+        VCS.print ();
+        RespBuiltProof(rc,time)
+
+  let check_task_aux extra name l i =
+    match List.nth l i with
+    | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) ->
+        Pp.msg_info(
+          str(Printf.sprintf "Checking task %d (%s%s) of %s" i s extra name));
+        VCS.restore vcs;
+        try
+          !reach_known_state ~cache:`No eop;
+          (* The original terminator, a hook, has not been saved in the .vi*)
+          Proof_global.set_terminator
+            (Lemmas.standard_proof_terminator [] (fun _ _ -> ()));
+          let proof = Proof_global.close_proof (fun x -> x) in
+          vernac_interp eop ~proof
+            { verbose = false; loc;
+              expr = (VernacEndProof (Proved (true,None))) };
+          Some proof
+        with e ->
+          let e = Errors.push e in
+          (try match Stateid.get e with
+          | None ->
+              Pp.pperrnl Pp.(
+                str"File " ++ str name ++ str ": proof of " ++ str s ++
+                spc () ++ print e)
+          | Some (_, cur) ->
+              match VCS.visit cur with
+              | { step = `Cmd ( { loc }, _) } 
+              | { step = `Fork ( { loc }, _, _, _) } 
+              | { step = `Qed ( { qast = { loc } }, _) } 
+              | { step = `Sideff (`Ast ( { loc }, _)) } ->
+                  let start, stop = Loc.unloc loc in
+                  Pp.pperrnl Pp.(
+                    str"File " ++ str name ++ str ": proof of " ++ str s ++
+                    str ": chars " ++ int start ++ str "-" ++ int stop ++
+                    spc () ++ print e)
+              | _ ->
+                  Pp.pperrnl Pp.(
+                    str"File " ++ str name ++ str ": proof of " ++ str s ++
+                    spc () ++ print e)
+        with e ->
+          Pp.msg_error (str"unable to print error message: " ++
+                        str (Printexc.to_string e))); None
+
+  let finish_task name (u,cst,_) d p l i =
+    let bucket =
+      match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in
+    match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
+    | None -> exit 1
+    | Some (po,pt) ->
+        let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
+        let con =
+          Nametab.locate_constant
+            (Libnames.qualid_of_ident po.Proof_global.id) in
+        let c = Global.lookup_constant con in
+        match c.Declarations.const_body with
+        | Declarations.OpaqueDef lc ->
+            let uc = Option.get (Opaqueproof.get_constraints lc) in
+            let uc =
+              Future.chain ~greedy:true ~pure:true uc Univ.hcons_constraints in
+            let pr = Opaqueproof.get_proof lc 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.sink pr;
+            let extra = Future.join uc in
+            u.(bucket) <- uc;
+            p.(bucket) <- pr;
+            u, Univ.union_constraints cst extra, false
+        | _ -> assert false
+  
+  let check_task name l i =
+    match check_task_aux "" name l i with
+    | Some _ -> true
+    | None -> false
+
+  let info_tasks l =
+    CList.map_i (fun i (ReqBuildProof(_,_,_,loc,_,s)) ->
+      let time1 =
+        try float_of_string (Aux_file.get !hints loc "proof_build_time")
+        with Not_found -> 0.0 in
+      let time2 =
+        try float_of_string (Aux_file.get !hints loc "proof_check_time")
+        with Not_found -> 0.0 in
+      s,max (time1 +. time2) 0.0001,i) 0 l
+
+  open Interface
+
+  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 : Future.UUID.t 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 (Marshal.from_channel ic : Future.UUID.t 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 (Marshal.from_channel ic : more_data)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_more_data: "^s)
+
+  let queue : task TQueue.t = TQueue.create ()
+
+  let set_perspective idl =
+    let open Stateid in
+    let p = List.fold_right Set.add idl Set.empty in
+    TQueue.reorder queue (fun task1 task2 ->
+      let TaskBuildProof (_, a1, b1, _, _,_,_,_) = task1 in
+      let TaskBuildProof (_, a2, b2, _, _,_,_,_) = task2 in
+      match Set.mem a1 p || Set.mem b1 p, Set.mem a2 p || Set.mem b2 p with
+      | true, true | false, false -> 0
+      | true, false -> -1
+      | false, true -> 1)
+
+  let wait_all_done () =
+    if not (WorkersPool.is_empty ()) then
+      TQueue.wait_until_n_are_waiting_and_queue_empty
+        (WorkersPool.n_workers ()) queue
+
+  let build_proof ~loc ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
+    let cancel_switch = ref false in
+    if WorkersPool.is_empty () then
+      if !Flags.compilation_mode = Flags.BuildVi then begin
+        let force () : Entries.proof_output list Future.assignement =
+          try `Val (build_proof_here_core loc stop ())
+          with e -> let e = Errors.push e in `Exn e in
+        let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
+        let uuid = Future.uuid f in
+        TQueue.push queue (TaskBuildProof
+          (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
+        f, cancel_switch
+      end else
+        build_proof_here exn_info loc stop, cancel_switch
+    else 
+      let f, assign = Future.create_delegate (State.exn_on id ~valid) in
+      let uuid = Future.uuid f in
+      Pp.feedback (Interface.InProgress 1);
+      TQueue.push queue (TaskBuildProof
+        (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
+      f, cancel_switch
+
+  exception RemoteException of std_ppcmds
+  let _ = Errors.register_handler (function
+    | RemoteException ppcmd -> ppcmd
+    | _ -> raise Unhandled)
+
+  exception KillRespawn
+    
+  let report_status ?id s =
+    let id =
+      match id with
+      | Some n -> n
+      | None ->
+          match !Flags.async_proofs_mode with
+          | Flags.APonParallel n -> n
+          | _ -> assert false in
+    Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s))
+
+  let rec manage_slave ~cancel:cancel_user_req id_slave respawn =
+    let ic, oc, proc =
+      let rec set_slave_opt = function
+        | [] -> ["-async-proofs"; "worker"; string_of_int id_slave; "-feedback-glob"]
+        | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl
+        | ("-async-proofs"
+          |"-compile"
+          |"-compile-verbose")::_::tl -> set_slave_opt tl
+        | x::tl -> x :: set_slave_opt tl in
+      let args =
+        Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
+      let env =
+        Array.append !async_proofs_workers_extra_env (Unix.environment ()) in
+      respawn ~args ~env () in
+    let last_task = ref None in
+    let task_expired = ref false in
+    let task_cancelled = ref false in
+    CThread.prepare_in_channel_for_thread_friendly_io ic;
+    try
+      while true do
+        prerr_endline "waiting for a task";
+        report_status ~id:id_slave "Idle";
+        let task = TQueue.pop queue in
+        prerr_endline ("got task: "^pr_task task);
+        last_task := Some task;
+        try
+          marshal_request oc (request_of_task task);
+          let cancel_switch = cancel_switch_of_task task in
+          Worker.kill_if proc ~sec:1 (fun () ->
+            task_expired := !cancel_switch;
+            task_cancelled := !cancel_user_req;
+            if !cancel_user_req then cancel_user_req := false;
+            !task_expired || !task_cancelled);
+          let rec loop () =
+            let response = unmarshal_response ic in
+            match task, response with
+            | TaskBuildProof(_,_,_, assign,_,loc,_,s),
+              RespBuiltProof(pl, time)->
+                assign (`Val pl);
+                (* We restart the slave, to avoid memory leaks.  We could just
+                   Pp.feedback (Interface.InProgress ~-1) *)
+                record_pb_time s loc time;
+                last_task := None;
+                raise KillRespawn
+            | TaskBuildProof(_,_,_, assign,_,_,_,_),
+              RespError(err_id,valid,e,valid_states) ->
+                let e = Stateid.add ~valid (RemoteException e) err_id in
+                assign (`Exn e);
+                List.iter (fun (id,s) -> State.assign id s) valid_states;
+                (* We restart the slave, to avoid memory leaks.  We could just
+                   Pp.feedback (Interface.InProgress ~-1) *)
+                last_task := None;
+                raise KillRespawn
+            | _, RespGetCounterFreshLocalUniv ->
+                marshal_more_data oc (MoreDataLocalUniv
+                  (CList.init 10 (fun _ -> Univ.fresh_local_univ ())));
+                if !cancel_switch then raise KillRespawn else loop ()
+            | _, RespGetCounterNewUnivLevel ->
+                marshal_more_data oc (MoreDataUnivLevel
+                  (CList.init 10 (fun _ -> Termops.new_univ_level ())));
+                loop ()
+            | _, RespFeedback {id = State state_id; content = msg} ->
+                Pp.feedback ~state_id msg;
+                loop ()
+            | _, RespFeedback _ -> assert false (* Parsing in master process *)
+          in
+            loop ()
+        with
+        | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *)
+            Pp.feedback (Interface.InProgress ~-1);
+            prerr_endline ("Task expired: " ^ pr_task task)
+        | (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e ->
+            raise e (* we pass the exception to the external handler *)
+        | MarshalError s when !fallback_to_lazy_if_marshal_error ->
+            msg_warning(strbrk("Marshalling error: "^s^". "^
+              "The system state could not be sent to the worker process. "^
+              "Falling back to local, lazy, evaluation."));
+            let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
+            assign(`Comp(build_proof_here exn_info loc stop));
+            Pp.feedback (Interface.InProgress ~-1)
+        | MarshalError s ->
+            pr_err ("Fatal marshal error: " ^ s);
+            flush_all (); exit 1
+        | e ->
+            pr_err ("Uncaught exception in worker manager: "^
+              string_of_ppcmds (print e));
+            flush_all ()
+      done
+    with
+    | KillRespawn ->
+        Pp.feedback (Interface.InProgress ~-1);
+        Worker.kill proc; ignore(Worker.wait proc);
+        manage_slave ~cancel:cancel_user_req id_slave respawn
+    | Sys_error _ | Invalid_argument _ | End_of_file when !task_expired ->
+        Pp.feedback (Interface.InProgress ~-1);
+        ignore(Worker.wait proc);
+        manage_slave ~cancel:cancel_user_req id_slave respawn
+    | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled ->
+        msg_warning(strbrk "The worker was cancelled.");
+        Option.iter (fun task ->
+          let TaskBuildProof (_, start, _, assign, _,_,_,_) = task in
+          let s = "Worker cancelled by the user" in
+          let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in
+          assign (`Exn e);
+          Pp.feedback ~state_id:start (Interface.ErrorMsg (Loc.ghost, s));
+          Pp.feedback (Interface.InProgress ~-1);
+        ) !last_task;
+        Worker.kill proc; ignore(Worker.wait proc);
+        manage_slave ~cancel:cancel_user_req id_slave respawn
+    | Sys_error _ | Invalid_argument _ | End_of_file
+      when !fallback_to_lazy_if_slave_dies ->
+        msg_warning(strbrk "The worker process died badly.");
+        Option.iter (fun task ->
+          msg_warning(strbrk "Falling back to local, lazy, evaluation.");
+          let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
+          assign(`Comp(build_proof_here exn_info loc stop));
+          Pp.feedback (Interface.InProgress ~-1);
+        ) !last_task;
+        Worker.kill proc; ignore(Worker.wait proc);
+        manage_slave ~cancel:cancel_user_req id_slave respawn
+    | Sys_error _ | Invalid_argument _ | End_of_file ->
+        Worker.kill proc;
+        let exit_status proc = 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
+        pr_err ("Fatal worker error: " ^ (exit_status proc));
+        flush_all (); exit 1
+
+  let init () = WorkersPool.init !Flags.async_proofs_n_workers manage_slave
+
+  let slave_ic = ref stdin
+  let slave_oc = ref stdout
+
+  let slave_init_stdout () =
+    let ic, oc = Spawned.get_channels () in
+    slave_oc := oc; slave_ic := ic
+
+  let bufferize f =
+    let l = ref [] in
+    fun () ->
+      match !l with
+      | [] -> let data = f () in l := List.tl data; List.hd data
+      | x::tl -> l := tl; x
+
+  let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc
+
+  let slave_main_loop reset =
+    let slave_feeder oc fb =
+      Marshal.to_channel oc (RespFeedback fb) [];
+      flush oc in
+    Pp.set_feeder (slave_feeder !slave_oc);
+    Termops.set_remote_new_univ_level (bufferize (fun () ->
+      marshal_response !slave_oc RespGetCounterNewUnivLevel;
+      match unmarshal_more_data !slave_ic with
+      | MoreDataUnivLevel l -> l | _ -> assert false));
+    Univ.set_remote_fresh_local_univ (bufferize (fun () ->
+      marshal_response !slave_oc RespGetCounterFreshLocalUniv;
+      match unmarshal_more_data !slave_ic with
+      | MoreDataLocalUniv l -> l | _ -> assert false));
+    let working = ref false in
+    slave_handshake ();
+    while true do
+      try
+        working := false;
+        let request = unmarshal_request !slave_ic in
+        working := true;
+        report_status (name_of_request request);
+        let response = slave_respond request in
+        report_status "Idle";
+        marshal_response !slave_oc response;
+        reset ()
+      with
+      | MarshalError s ->
+        pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+      | End_of_file ->
+        prerr_endline "connection lost"; flush_all (); exit 2
+      | e when Errors.noncritical e ->
+        (* This can happen if the proof is broken.  The error has also been
+         * signalled as a feedback, hence we can silently recover *)
+        let err_id, safe_id = match Stateid.get e with
+          | Some (safe, err) -> err, safe
+          | None -> Stateid.dummy, Stateid.dummy in
+        prerr_endline "failed with the following exception:";
+        prerr_endline (string_of_ppcmds (print e));
+        prerr_endline ("last safe id is: " ^ Stateid.to_string safe_id);
+        prerr_endline ("cached? " ^ string_of_bool (State.is_cached safe_id));
+        let prog old_v n =
+          if n < 3 then n else old_v + n/3 + if n mod 3 > 0 then 1 else 0 in
+        let states =
+          let open State in
+          let rec aux n m prev_id =
+            let next =
+              try Some (VCS.visit prev_id).next
+              with VCS.Expired -> None in
+            match next with
+            | None -> []
+            | Some id when n = m ->
+                prerr_endline ("sending back state " ^  string_of_int m);
+                let tail = aux (n+1) (prog m (n+1)) id in
+                if is_cached id then (id, get_cached id) :: tail else tail
+            | Some id -> aux (n+1) m id in
+          (if is_cached safe_id then [safe_id,get_cached safe_id] else [])
+          @ aux 1 (prog 1 1) safe_id in
+        marshal_response !slave_oc (RespError(err_id, safe_id, print e, states))
+      | e ->
+        pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+        flush_all (); exit 1
+    done
+
+  (* For external users this name is nicer than request *)
+  type tasks = int request list
+  let dump f2t_map =
+    assert(WorkersPool.is_empty ()); (* ATM, we allow that only if no slaves *)
+    let tasks = TQueue.dump queue in
+    prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks));
+    let tasks = List.map request_of_task tasks in
+    List.map (function ReqBuildProof(a,b,c,d,x,e) ->
+      ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks
+
+end (* }}} *)
+
+(* Runs all transactions needed to reach a state *)
+module Reach : sig
+
+  val known_state :
+    ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
+
+end = struct (* {{{ *)
+
+let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
+
+let delegate_policy_check time =
+  if interactive () = `Yes then
+    (!Flags.async_proofs_mode = Flags.APonParallel 0 ||
+    !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0
+  else if !Flags.compilation_mode = Flags.BuildVi then true
+  else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0
+
+let collect_proof cur hd brkind id =
+ prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ let no_name = "" in
+ let name = function
+   | [] -> no_name
+   | id :: _ -> Id.to_string id in
+ let loc = (snd cur).loc in
+ let is_defined = function
+   | _, { expr = VernacEndProof (Proved (false,_)) } -> true
+   | _ -> false in
+ let rec collect last accn id =
+    let view = VCS.visit id in
+    match last, view.step with
+    | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
+    | _, `Alias _ -> `Sync (no_name,`Alias)
+    | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs)
+    | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) ->
+        `Sync (no_name,`Doesn'tGuaranteeOpacity)
+    | Some (parent, ({ expr = VernacProof(_,Some _)} as v)),
+      `Fork (_, hd', GuaranteesOpacity, ids) ->
+        let name = name ids in
+        let time = get_hint_bp_time name in
+        assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
+        if delegate_policy_check time
+        then `ASync (parent,Some v,accn,name)
+        else `Sync (name,`Policy)
+    | Some (parent, ({ expr = VernacProof(t,None)} as v)),
+      `Fork (_, hd', GuaranteesOpacity, ids) when
+       not (State.is_cached parent) &&
+       !Flags.compilation_mode = Flags.BuildVi ->
+        (try
+          let name = name ids in
+          let hint, time = get_hint_ctx loc, get_hint_bp_time name in
+          assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
+          v.expr <- VernacProof(t, Some hint);
+          if delegate_policy_check time
+          then `ASync (parent,Some v,accn,name)
+          else `Sync (name,`Policy)
+        with Not_found -> `Sync (no_name,`NoHint))
+    | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
+        assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
+        let name = name ids in
+        let time = get_hint_bp_time name in
+        if delegate_policy_check time
+        then `MaybeASync (parent, accn, name)
+        else `Sync (name,`Policy)
+    | _, `Sideff _ -> `Sync (no_name,`NestedProof)
+    | _ -> `Sync (no_name,`Unknown) in
+ match cur, (VCS.visit id).step, brkind with
+ |( parent, { expr = VernacExactProof _ }), `Fork _, _ ->
+     `Sync (no_name,`Immediate)
+ | _, _, { VCS.kind = `Edit _ }  -> collect (Some cur) [] id
+ | _ ->
+     if is_defined cur then `Sync (no_name,`Transparent)
+     else
+       let rc = collect (Some cur) [] id in
+       if not (State.is_cached id) then rc
+       else (* we already have the proof, no gain in delaying *)
+         match rc with
+         | `Sync(name,_) -> `Sync (name,`AlreadyEvaluated)
+         | `MaybeASync(_,_,name) -> `Sync (name,`AlreadyEvaluated)
+         | `ASync(_,_,_,name) -> `Sync (name,`AlreadyEvaluated)
+
+let string_of_reason = function
+  | `Transparent -> "Transparent"
+  | `AlreadyEvaluated -> "AlreadyEvaluated"
+  | `Policy -> "Policy"
+  | `NestedProof -> "NestedProof"
+  | `Immediate -> "Immediate"
+  | `Alias -> "Alias"
+  | `NoHint -> "NoHint"
+  | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
+  | _ -> "Unknown Reason"
+
+let wall_clock_last_fork = ref 0.0
+
+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 inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
+
+  let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
+    prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
+    reach id;
+    cherry_pick_non_pstate ()) id
+
+  (* traverses the dag backward from nodes being already calculated *)
+  and reach ?(redefine_qed=false) ?(cache=cache) id =
+    prerr_endline ("reaching: " ^ Stateid.to_string id);
+    if not redefine_qed && State.is_cached id then begin
+      State.install_cached id;
+      feedback ~state_id:id Interface.Processed;
+      prerr_endline ("reached (cache)")
+    end else
+    let step, cache_step =
+      let view = VCS.visit id in
+      match view.step with
+      | `Alias id -> (fun () ->
+            reach view.next; reach id
+          ), cache
+      | `Cmd (x,_) -> (fun () ->
+            reach view.next; vernac_interp id x
+          ), cache
+      | `Fork (x,_,_,_) -> (fun () ->
+            reach view.next; vernac_interp id x;
+            wall_clock_last_fork := Unix.gettimeofday ()
+          ), `Yes
+      | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
+          let rec aux = function
+          | `ASync (start, proof_using_ast, nodes, name) -> (fun () ->
+                prerr_endline ("Asynchronous " ^ Stateid.to_string id);
+                VCS.create_cluster nodes ~tip:id;
+                begin match keep, brinfo, qed.fproof with
+                | VtKeep, { VCS.kind = `Edit _ }, None -> assert false
+                | VtKeep, { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
+                    assert(redefine_qed = true);
+                    VCS.create_cluster nodes ~tip:id;
+                    let fp, cancel = Slaves.build_proof
+                      ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in
+                    Future.replace ofp fp;
+                    qed.fproof <- Some (fp, cancel)
+                | VtKeep, { VCS.kind = `Proof _ }, Some _ -> assert false
+                | VtKeep, { VCS.kind = `Proof _ }, None ->
+                    reach ~cache:`Shallow start;
+                    let fp, cancel = Slaves.build_proof
+                      ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in
+                    qed.fproof <- Some (fp, cancel);
+                    let proof =
+                      Proof_global.close_future_proof ~feedback_id:id fp in
+                    reach view.next;
+                    vernac_interp id ~proof x;
+                    feedback ~state_id:id Interface.Incomplete
+                | VtDrop, _, _ ->
+                    reach view.next;
+                    Option.iter (vernac_interp start) proof_using_ast;
+                    vernac_interp id x
+                | _, { VCS.kind = `Master }, _ -> assert false
+                end;
+                Proof_global.discard_all ()
+              ), if redefine_qed then `No else `Yes
+          | `Sync (name, `Immediate) -> (fun () -> 
+                assert (Stateid.equal view.next eop);
+                reach eop; vernac_interp id x; Proof_global.discard_all ()
+              ), `Yes
+          | `Sync (name, reason) -> (fun () ->
+                prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^
+                  string_of_reason reason);
+                reach eop;
+                let wall_clock = Unix.gettimeofday () in
+                record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
+                begin match keep with
+                | VtKeep ->
+                    let proof =
+                      Proof_global.close_proof (State.exn_on id ~valid:eop) in
+                    reach view.next;
+                    let wall_clock2 = Unix.gettimeofday () in
+                    vernac_interp id ~proof x;
+                    let wall_clock3 = Unix.gettimeofday () in
+                    Aux_file.record_in_aux_at x.loc "proof_check_time"
+                      (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2))
+                | VtDrop ->
+                    reach view.next;
+                    vernac_interp id x
+                end;
+                Proof_global.discard_all ()
+              ), `Yes
+          | `MaybeASync (start, nodes, name) -> (fun () ->
+                prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
+                reach ~cache:`Shallow start;
+                (* no sections *)
+                if List.is_empty (Environ.named_context (Global.env ()))
+                then fst (aux (`ASync (start, None, nodes, name))) ()
+                else fst (aux (`Sync (name, `Unknown))) ()
+              ), if redefine_qed then `No else `Yes
+          in
+          aux (collect_proof (view.next, x) brname brinfo eop)
+      | `Sideff (`Ast (x,_)) -> (fun () ->
+            reach view.next; vernac_interp id x
+          ), cache
+      | `Sideff (`Id origin) -> (fun () ->
+            let s = pure_cherry_pick_non_pstate origin in
+            reach view.next;
+            inject_non_pstate s
+          ), cache
+    in
+    if !Flags.async_proofs_mode = Flags.APonParallel 0 then
+      Pp.feedback ~state_id:id Interface.ProcessingInMaster;
+    State.define ~cache:cache_step ~redefine:redefine_qed step id;
+    prerr_endline ("reached: "^ Stateid.to_string id) in
+  reach ~redefine_qed id
+
+end (* }}} *)
+let _ = Slaves.set_reach_known_state Reach.known_state
+
+(* The backtrack module simulates the classic behavior of a linear document *)
+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
+
+end = struct (* {{{ *)
+
+  let record () =
+    let current_branch = VCS.current_branch () in
+    let mine = current_branch, VCS.get_branch current_branch in
+    let info = VCS.get_info (VCS.get_branch_pos current_branch) in
+    let others =
+      CList.map_filter (fun b ->
+        if Vcs_.Branch.equal b current_branch then None
+        else Some(b, VCS.get_branch b)) (VCS.branches ()) in
+    info.vcs_backup <- Some (VCS.backup ()), Some { mine; others }
+
+  let backto oid =
+    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")
+    | Some vcs, _ ->
+        VCS.restore vcs;
+        let id = VCS.get_branch_pos (VCS.current_branch ()) in
+        if not (Stateid.equal id oid) then
+          anomaly (str "Backtrack.backto did not jump to the right state")
+
+  let branches_of id =
+    let info = VCS.get_info id in
+    match info.vcs_backup with
+    | _, None ->
+       anomaly(str"Backtrack.backto "++str(Stateid.to_string id)++
+               str": a state with no vcs_backup")
+    | _, Some x -> x
+
+  let rec fold_until f acc id =
+    let next acc =
+      if id = Stateid.initial then raise Not_found
+      else fold_until f acc (VCS.visit id).next in
+    let info = VCS.get_info id in
+    match info.vcs_backup with
+    | None, _ -> next acc
+    | Some vcs, _ ->
+        let ids =
+          if id = Stateid.initial || id = Stateid.dummy then [] else
+          match VCS.visit id with
+          | { step = `Fork (_,_,_,l) } -> l
+          | { step = `Cmd (_,l) } -> l
+          | _ -> [] in
+        match f acc (id, vcs, ids) with
+        | `Stop x -> x
+        | `Cont acc -> next acc
+ 
+  let back_safe () =
+    let id =
+      fold_until (fun n (id,_,_) ->
+        if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
+        0 (VCS.get_branch_pos (VCS.current_branch ())) in
+    backto id
+
+  let undo_vernac_classifier v =
+    try
+      match v with
+      | VernacResetInitial ->
+          VtStm (VtBack Stateid.initial, true), VtNow
+      | VernacResetName (_,name) ->
+          msg_warning
+            (str"Reset not implemented for automatically generated constants");
+          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
+          with Not_found ->
+            VtStm (VtBack id, true), 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
+      | VernacUndo 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), 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")
+            | Some vcs, _ -> vcs in
+          let cb, _ =
+            Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
+          let n = fold_until (fun n (_,vcs,_) ->
+            if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
+            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
+      | 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
+      | VernacBacktrack (id,_,_)
+      | VernacBackTo id ->
+          VtStm (VtBack (Stateid.of_int id), true), VtNow
+      | _ -> VtUnknown, VtNow
+    with
+    | Not_found ->
+       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
+       VtStm (VtBack Stateid.initial, true), VtNow
+
+end (* }}} *)
+
+let init () =
+  VCS.init Stateid.initial;
+  set_undo_classifier Backtrack.undo_vernac_classifier;
+  State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
+  Backtrack.record ();
+  if !Flags.async_proofs_mode = Flags.APonParallel 0 then begin
+    Slaves.init ();
+    let opts = match !Flags.async_proofs_worker_flags with
+      | None -> []
+      | Some s -> Str.split_delim (Str.regexp ",") s in
+    if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then
+      fallback_to_lazy_if_marshal_error := false;
+    if String.List.mem "fallback-to-lazy-if-slave-dies=no" opts then
+      fallback_to_lazy_if_slave_dies := false;
+    begin try
+      let env_opt = Str.regexp "^extra-env=" in
+      let env = List.find (fun s -> Str.string_match env_opt s 0) opts in
+      async_proofs_workers_extra_env := Array.of_list
+        (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
+    with Not_found -> () end;
+  end
+
+let slave_main_loop () = Slaves.slave_main_loop Ephemeron.clear
+
+let slave_init_stdout () = Slaves.slave_init_stdout ()
+
+let observe id =
+  let vcs = VCS.backup () in
+  try
+    Reach.known_state ~cache:(interactive ()) id;
+    VCS.print ()
+  with e ->
+    let e = Errors.push e in
+    VCS.print ();
+    VCS.restore vcs;
+    raise e
+
+let finish () =
+  observe (VCS.get_branch_pos (VCS.current_branch ()));
+  VCS.print ()
+
+let wait () =
+  Slaves.wait_all_done ();
+  VCS.print ()
+
+let join () =
+  let rec jab id =
+    if Stateid.equal id Stateid.initial then ()
+    else
+      let view = VCS.visit id in
+      match view.step with
+      | `Qed ({ keep = VtDrop }, eop) ->
+           Future.purify observe eop; jab view.next
+      | _ -> jab view.next in
+  finish ();
+  wait ();
+  prerr_endline "Joining the environment";
+  Global.join_safe_environment ();
+  VCS.print ();
+  prerr_endline "Joining the aborted proofs";
+  jab (VCS.get_branch_pos VCS.Branch.master);
+  VCS.print ()
+
+type tasks = Slaves.tasks * RemoteCounter.remote_counters_status
+let dump x = Slaves.dump x, RemoteCounter.backup ()
+let check_task name (tasks,_) i =
+  let vcs = VCS.backup () in
+  try
+    let rc = Future.purify (Slaves.check_task name tasks) i in
+    Pp.pperr_flush ();
+    VCS.restore vcs;
+    rc
+  with e when Errors.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
+    Pp.pperr_flush ();
+    VCS.restore vcs;
+    u in
+  try
+    let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
+    (u,a,true), p
+  with e ->
+    let e = Errors.push e in
+    Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
+    exit 1
+
+let merge_proof_branch qast keep brname =
+  let brinfo = VCS.get_branch brname in
+  let qed fproof = { qast; keep; brname; brinfo; fproof } in
+  match brinfo with
+  | { VCS.kind = `Proof _ } ->
+      VCS.checkout VCS.Branch.master;
+      let id = VCS.new_node () in
+      VCS.merge id ~ours:(Qed (qed None)) brname;
+      VCS.delete_branch brname;
+      if keep == VtKeep then VCS.propagate_sideff None;
+      `Ok
+  | { VCS.kind = `Edit (mode, qed_id, master_id) } ->
+      let ofp =
+        match VCS.visit qed_id with
+        | { step = `Qed ({ fproof }, _) } -> fproof
+        | _ -> assert false in
+      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;
+      VCS.checkout VCS.Branch.master;
+      `Unfocus qed_id
+  | { VCS.kind = `Master } ->
+       raise (State.exn_on Stateid.dummy Proof_global.NoCurrentProof)
+
+(* 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 vcs tty =
+  match Stateid.get e 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() ++
+        Errors.print_no_report e)
+  | Some (safe_id, id) ->
+      prerr_endline ("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 ();
+      raise e
+
+let process_transaction ~tty verbose c (loc, expr) =
+  let warn_if_pos a b =
+    if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
+  let v, x = expr, { verbose = verbose && Flags.is_verbose(); loc; expr } in
+  prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  let vcs = VCS.backup () in
+  try
+    let head = VCS.current_branch () in
+    VCS.checkout head;
+    let rc = begin
+      prerr_endline ("  classified as: " ^ 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 -> warn_if_pos x b; join (); `Ok
+      | VtStm (VtFinish, b),       VtNow -> warn_if_pos x b; finish (); `Ok
+      | VtStm (VtWait, b),     VtNow -> warn_if_pos x b; finish (); wait (); `Ok
+      | VtStm (VtPrintDag, b), VtNow ->
+          warn_if_pos x b; VCS.print ~now:true (); `Ok
+      | VtStm (VtObserve id, b),   VtNow -> warn_if_pos x b; 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 () in
+          let { mine; others } = Backtrack.branches_of oid in
+          List.iter (fun branch ->
+            if not (List.mem_assoc branch (mine::others)) then
+              ignore(merge_proof_branch 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);
+            end)
+            (VCS.branches ());
+          VCS.checkout_shallowest_proof_branch ();
+          VCS.commit id (Alias oid);
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtStm (VtBack id, false), VtNow ->
+          prerr_endline ("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")
+
+      (* Query *)
+      | VtQuery false, VtNow when tty = true ->
+          finish ();
+          (try Future.purify (vernac_interp Stateid.dummy)
+                  { verbose = true; loc; expr }
+           with e when Errors.noncritical e ->
+             let e = Errors.push e in
+             raise(State.exn_on Stateid.dummy e)); `Ok
+      | VtQuery false, VtNow ->
+          (try vernac_interp Stateid.dummy x
+           with e when Errors.noncritical e ->
+             let e = Errors.push e in
+             raise(State.exn_on Stateid.dummy e)); `Ok
+      | VtQuery true, w ->
+          let id = VCS.new_node () in
+          VCS.commit id (Cmd (x,[]));
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtQuery false, VtLater ->
+          anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
+
+      (* Proof *)
+      | VtStartProof (mode, guarantee, names), w ->
+          let id = VCS.new_node () in
+          let bname = VCS.mk_branch_name x in
+          VCS.checkout VCS.Branch.master;
+          VCS.commit id (Fork (x, bname, guarantee, names));
+          VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
+          Proof_global.activate_proof_mode mode;
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtProofMode _, VtLater ->
+          anomaly(str"VtProofMode must be executed VtNow")
+      | VtProofMode mode, VtNow ->
+          let id = VCS.new_node () in
+          VCS.checkout VCS.Branch.master;
+          VCS.commit id (Cmd (x,[]));
+          VCS.propagate_sideff (Some x);
+          List.iter
+            (fun bn -> match VCS.get_branch bn with
+            | { VCS.root; kind = `Master; pos } -> ()
+            | { VCS.root; kind = `Proof(_,d); pos } ->
+                VCS.delete_branch bn;
+                VCS.branch ~root ~pos bn (`Proof(mode,d))
+            | { VCS.root; kind = `Edit(_,f,q); pos } ->
+                VCS.delete_branch bn;
+                VCS.branch ~root ~pos bn (`Edit(mode,f,q)))
+            (VCS.branches ());
+          VCS.checkout_shallowest_proof_branch ();
+          Backtrack.record ();
+          finish ();
+          `Ok
+      | VtProofStep, w ->
+          let id = VCS.new_node () in
+          VCS.commit id (Cmd (x,[]));
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtQed keep, w ->
+          let rc = merge_proof_branch x keep head in
+          VCS.checkout_shallowest_proof_branch ();
+          Backtrack.record (); if w == VtNow then finish ();
+          rc
+          
+      (* Side effect on all branches *)
+      | VtSideff l, w ->
+          let id = VCS.new_node () in
+          VCS.checkout VCS.Branch.master;
+          VCS.commit id (Cmd (x,l));
+          VCS.propagate_sideff (Some x);
+          VCS.checkout_shallowest_proof_branch ();
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+
+      (* Unknown: we execute it, check for open goals and propagate sideeff *)
+      | VtUnknown, VtNow ->
+          let id = VCS.new_node () in
+          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;
+            (* Vernac x may or may not start a proof *)
+            if VCS.Branch.equal head VCS.Branch.master &&
+               Proof_global.there_are_pending_proofs ()
+            then begin
+              let bname = VCS.mk_branch_name x in
+              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
+              VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
+              Proof_global.activate_proof_mode "Classic";
+            end else begin
+              VCS.commit id (Cmd (x,[]));
+              VCS.propagate_sideff (Some x);
+              VCS.checkout_shallowest_proof_branch ();
+            end in
+          State.define ~cache:`Yes step id;
+          Backtrack.record (); `Ok
+
+      | VtUnknown, VtLater ->
+          anomaly(str"classifier: VtUnknown must imply VtNow")
+    end in
+    (* Proof General *)
+    begin match v with 
+      | VernacStm (PGLast _) ->
+        if not (VCS.Branch.equal head VCS.Branch.master) then
+          vernac_interp Stateid.dummy
+            { verbose = true; loc = Loc.ghost;
+              expr = VernacShow (ShowGoal OpenSubgoals) }
+      | _ -> ()
+    end;
+    prerr_endline "processed }}}";
+    VCS.print ();
+    rc
+  with e ->
+    let e = Errors.push e in
+    handle_failure e vcs tty
+
+(** STM interface {{{******************************************************* **)
+
+let stop_worker n = Slaves.cancel_worker n
+
+let query ~at s =
+  Future.purify (fun s ->
+    if Stateid.equal at Stateid.dummy then finish ()
+    else Reach.known_state ~cache:`Yes at;
+    let _, ast as loc_ast = vernac_parse 0 s in
+    let clas = classify_vernac ast in
+    match clas with
+    | VtStm (w,_), _ ->
+       ignore(process_transaction
+         ~tty:false true (VtStm (w,false), VtNow) loc_ast)
+    | _ ->
+       ignore(process_transaction
+         ~tty:false true (VtQuery false, VtNow) loc_ast))
+  s
+
+let add ~ontop ?(check=ignore) verb eid s =
+  let cur_tip = VCS.cur_tip () in
+  if Stateid.equal ontop cur_tip then begin
+    let _, ast as loc_ast = vernac_parse eid s in
+    check(loc_ast);
+    let clas = classify_vernac ast in
+    match process_transaction ~tty:false verb clas loc_ast with
+    | `Ok -> VCS.cur_tip (), `NewTip
+    | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
+  end else begin
+    (* For now, arbitrary edits should be announced with edit_at *)
+    anomaly(str"Not yet implemented, the GUI should not try this")
+  end
+
+let set_perspective id_list = Slaves.set_perspective id_list
+
+type focus = {
+  start : Stateid.t;
+  stop : Stateid.t;
+  tip : Stateid.t
+}
+
+let edit_at 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 =
+      if id = cur then true
+      else match VCS.visit cur with
+      | { step = `Fork _ } -> false
+      | { next } -> aux next in
+    aux (VCS.get_branch_pos (VCS.current_branch ())) in
+  let is_ancestor_of_cur_branch id =
+    Vcs_.NodeSet.mem id
+      (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
+  let has_failed qed_id =
+    match VCS.visit qed_id with
+    | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp
+    | _ -> false in
+  let rec master_for_br root tip =
+      if Stateid.equal tip Stateid.initial then tip else
+      match VCS.visit tip with
+      | { next } when next = root -> root
+      | { step = `Fork _ } -> tip
+      | { step = `Sideff (`Ast(_,id)|`Id id) } -> id
+      | { next } -> master_for_br root next in
+  let reopen_branch at_id mode qed_id tip =
+    VCS.delete_cluster_of id;
+    let master_id =
+      match VCS.visit qed_id with
+      | { step = `Qed _; next = master_id } -> master_id
+      | _ -> anomaly (str "Cluster not ending with Qed") in
+    VCS.branch ~root:master_id ~pos:id
+      VCS.edit_branch (`Edit (mode, qed_id, master_id));
+    Reach.known_state ~cache:(interactive ()) id;
+    VCS.checkout_shallowest_proof_branch ();
+    `Focus { stop = qed_id; start = master_id; tip } in
+  let backto id =
+    List.iter VCS.delete_branch (VCS.branches ());
+    let ancestors = VCS.reachable id in
+    let { mine = brname, brinfo; others } = Backtrack.branches_of id in
+    List.iter (fun (name,{ VCS.kind = k; root; pos }) ->
+      if not(VCS.Branch.equal name VCS.Branch.master) &&
+         Vcs_.NodeSet.mem root ancestors then
+        VCS.branch ~root ~pos name k)
+      others;
+    VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id);
+    VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind;
+    VCS.delete_cluster_of id;
+    VCS.gc ();
+    Reach.known_state ~cache:(interactive ()) id;
+    VCS.checkout_shallowest_proof_branch ();
+    `NewTip in
+  try
+    let rc =
+      let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
+      let branch_info =
+        match snd (VCS.get_info id).vcs_backup with
+        | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m
+        | _ -> None in
+      match focused, VCS.cluster_of id, branch_info with
+      | _, Some _, None -> assert false
+      | false, Some qed_id, Some mode ->
+          let tip = VCS.cur_tip () in
+          if has_failed qed_id then reopen_branch id mode qed_id tip
+          else backto id
+      | true, Some qed_id, Some mode ->
+          if on_cur_branch id then begin
+            assert false
+          end else if is_ancestor_of_cur_branch id then begin
+            backto id
+          end else begin
+            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;
+            VCS.checkout_shallowest_proof_branch ();
+            `NewTip
+          end else if is_ancestor_of_cur_branch id then begin
+            backto id
+          end else begin
+            anomaly(str"Cannot leave an `Edit branch open")
+          end
+      | false, None, _ -> backto id
+    in
+    VCS.print ();
+    rc
+  with e ->
+    let e = Errors.push e in
+    match Stateid.get e with
+    | None ->
+        VCS.print ();
+        anomaly (str ("edit_at: "^string_of_ppcmds (Errors.print_no_report e)))
+    | Some (_, id) ->
+        prerr_endline ("Failed at state " ^ Stateid.to_string id);
+        VCS.restore vcs;
+        VCS.print ();
+        raise e
+(* }}} *)
+
+(** Old tty interface {{{*************************************************** **)
+
+let interp verb (_,e as lexpr) =
+  let clas = classify_vernac e in
+  let rc = process_transaction ~tty:true verb clas lexpr 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
+    try finish ()
+    with e ->
+      let e = Errors.push e in
+      handle_failure e vcs true
+
+let get_current_state () = VCS.cur_tip ()
+
+let current_proof_depth () =
+  let head = VCS.current_branch () in
+  match VCS.get_branch head with
+  | { VCS.kind = `Master } -> 0
+  | { VCS.pos = cur; VCS.kind = (`Proof _ | `Edit _); VCS.root = root } ->
+      let rec distance root =
+        if Stateid.equal cur root then 0
+        else 1 + distance (VCS.visit cur).next in
+      distance cur
+
+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))
+
+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 (),  List.mem name 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 (x,_) -> find ((x.expr, (VCS.get_info id).n_goals)::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 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
+  with Vcs_aux.Expired -> ()
+
+(* }}} *)
+
+(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
new file mode 100644
index 000000000..a58100b5a
--- /dev/null
+++ b/stm/stm.mli
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Interface
+open Names
+
+(** 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]. *)
+val add : ontop:Stateid.t -> ?check:(located_vernac_expr -> unit) ->
+  bool -> edit_id -> string ->
+    Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* parses and xecutes a command at a given state, throws away its side effects
+   but for the printings *)
+val query : at:Stateid.t -> string -> 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
+   [id] is dropped by Coq.  [`Focus fo] is returned to say that [fo.tip] is the
+   new document tip, the document between [id] and [fo.stop] has been dropped.
+   The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
+   just to tell the gui where the editing zone starts, in case it wants to
+   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
+val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
+
+(* Evaluates the tip of the current branch *)
+val finish : unit -> unit
+
+val stop_worker : int -> unit
+
+(* Joins the entire document.  Implies finish, but also checks proofs *)
+val join : unit -> unit
+(* To save to disk an incomplete document *)
+type tasks
+val dump : (Future.UUID.t * int) list -> tasks
+
+val check_task : string -> tasks -> int -> bool
+val info_tasks : tasks -> (string * float * int) list
+val finish_tasks : string ->
+  Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+  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 slave_main_loop : unit -> unit
+val slave_init_stdout : unit -> unit
+
+(* 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
+
+(** read-eval-print loop compatible interface ****************************** **)
+
+(* Adds a new line to the document.  It replaces the core of Vernac.interp.
+   [finish] is called as the last bit of this function is the system
+   is running interactively (-emacs or coqtop). *)
+val interp : bool -> located_vernac_expr -> unit
+
+(* 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
+
+(** Reverse dependency hooks *)
+val process_error_hook : (exn -> exn) Hook.t
+val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
+  Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
new file mode 100644
index 000000000..347416099
--- /dev/null
+++ b/stm/stm.mllib
@@ -0,0 +1,9 @@
+Spawned
+Dag
+Vcs
+TQueue
+WorkerPool
+Vernac_classifier
+Lemmas
+Stm
+Vi_checking
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
new file mode 100644
index 000000000..783c545fd
--- /dev/null
+++ b/stm/tQueue.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type 'a t = {
+  queue: 'a Queue.t;
+  lock : Mutex.t;
+  cond : Condition.t;
+  mutable nwaiting : int;
+  cond_waiting : Condition.t;
+}
+
+let create () = {
+  queue = Queue.create ();
+  lock = Mutex.create ();
+  cond = Condition.create ();
+  nwaiting = 0;
+  cond_waiting = Condition.create ();
+}
+
+let pop ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) =
+  Mutex.lock m;
+  while Queue.is_empty q do
+    tq.nwaiting <- tq.nwaiting + 1;
+    Condition.signal cn;
+    Condition.wait c m;
+    tq.nwaiting <- tq.nwaiting - 1;
+  done;
+  let x = Queue.pop q in
+  Condition.signal c;
+  Condition.signal cn;
+  Mutex.unlock m;
+  x
+
+let push { queue = q; lock = m; cond = c } x =
+  Mutex.lock m;
+  Queue.push x q;
+  Condition.signal c;
+  Mutex.unlock m
+
+let wait_until_n_are_waiting_and_queue_empty j tq =
+  Mutex.lock tq.lock;
+  while not (Queue.is_empty tq.queue) || tq.nwaiting < j do
+    Condition.wait tq.cond_waiting tq.lock
+  done;
+  Mutex.unlock tq.lock
+
+let dump { queue; lock } =
+  let l = ref [] in
+  Mutex.lock lock;
+  while not (Queue.is_empty queue) do l := Queue.pop queue :: !l done;
+  Mutex.unlock lock;
+  List.rev !l
+
+let reorder tq rel =
+  Mutex.lock tq.lock;
+  let l = ref [] in
+  while not (Queue.is_empty tq.queue) do l := Queue.pop tq.queue :: !l done;
+  List.iter (fun x -> Queue.push x tq.queue) (List.sort rel !l);
+  Mutex.unlock tq.lock
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
new file mode 100644
index 000000000..a3ea5532f
--- /dev/null
+++ b/stm/tQueue.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Thread safe queue with some extras *)
+
+type 'a t
+val create : unit -> 'a t
+val pop : 'a t -> 'a
+val push : 'a t -> 'a -> unit
+val reorder : 'a t -> ('a -> 'a -> int) -> unit
+val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
+val dump : 'a t -> 'a list
diff --git a/stm/vcs.ml b/stm/vcs.ml
new file mode 100644
index 000000000..e2513b1c1
--- /dev/null
+++ b/stm/vcs.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+
+module type S = sig
+
+  module Branch :
+  sig
+    type t
+    val make : string -> t
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val to_string : t -> string
+    val master : t
+  end
+
+  type id
+
+  (* Branches have [branch_info] attached to them. *)
+  type ('kind) branch_info = {
+    kind : [> `Master] as 'kind;
+    root : id;
+    pos  : id;
+  }
+
+  type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
+
+  val empty : id -> ('kind,'diff,'info) t
+
+  val current_branch : ('k,'e,'i) t -> Branch.t
+  val branches : ('k,'e,'i) t -> Branch.t list
+
+  val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
+  val branch :
+    ('kind,'e,'i) t -> ?root:id -> ?pos:id ->
+        Branch.t -> 'kind -> ('kind,'e,'i) t
+  val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+  val merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i) t
+  val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
+  val rewrite_merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+            Branch.t -> ('k,'diff,'i) t
+  val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+
+  val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
+  val get_info : ('k,'e,'info) t -> id -> 'info option
+  
+  module NodeSet : Set.S with type elt = id
+
+  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+
+  val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+
+  module Dag : Dag.S with type node = id
+  val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t
+
+  val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t
+  val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option
+  val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t 
+
+end
+
+module Make(OT : Map.OrderedType) = struct
+
+module Dag = Dag.Make(OT)
+
+type id = OT.t
+
+module NodeSet = Dag.NodeSet
+
+
+module Branch =
+struct
+  type t = string
+  let make =
+    let bid = ref 0 in
+    fun s -> incr bid; string_of_int !bid ^ "_" ^ s
+  let equal = CString.equal
+  let compare = CString.compare
+  let to_string s = s
+  let master = "master"
+end
+
+module BranchMap = Map.Make(Branch)
+
+type 'kind branch_info = {
+  kind : [> `Master] as 'kind;
+  root : id;
+  pos  : id;
+}
+
+type ('kind,'edge,'info) t = {
+  cur_branch   : Branch.t;
+  heads        : 'kind branch_info BranchMap.t;
+  dag          : ('edge,'info,id) Dag.t;
+}
+
+let empty root = {
+  cur_branch = Branch.master;
+  heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master };
+  dag = Dag.empty;
+}
+
+let add_node vcs id edges =
+  assert (not (CList.is_empty edges));
+  { vcs with dag =
+     List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges }
+
+let get_branch vcs head =
+  try BranchMap.find head vcs.heads
+  with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
+
+let reset_branch vcs head id =
+  let map name h =
+    if Branch.equal name head then { h with pos = id } else h
+  in
+  { vcs with heads = BranchMap.mapi map vcs.heads; }
+
+let current_branch vcs = vcs.cur_branch
+
+let branch
+  vcs ?(root=(get_branch vcs vcs.cur_branch).pos) ?(pos=root) name kind
+=
+  { vcs with
+      heads = BranchMap.add name { kind; root; pos } vcs.heads;
+      cur_branch = name }
+
+let delete_branch vcs name =
+  if Branch.equal Branch.master name then vcs else
+  let filter n _ = not (Branch.equal n name) in
+  { vcs with heads = BranchMap.filter filter vcs.heads }
+
+let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name =
+  assert (not (Branch.equal name into));
+  let br_id = (get_branch vcs name).pos in
+  let cur_id = (get_branch vcs into).pos in
+  let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
+  let vcs = reset_branch vcs into id in
+  vcs
+
+let del_edge id vcs tgt = { vcs with dag = Dag.del_edge vcs.dag id tgt }
+
+let rewrite_merge vcs id ~ours:tr1 ~theirs:tr2 ~at:cur_id name =
+  let br_id = (get_branch vcs name).pos in
+  let old_edges = List.map fst (Dag.from_node vcs.dag id) in
+  let vcs = List.fold_left (del_edge id) vcs old_edges in
+  let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
+  vcs
+
+let commit vcs id tr =
+  let vcs = add_node vcs id [tr, (get_branch vcs vcs.cur_branch).pos] in
+  let vcs = reset_branch vcs vcs.cur_branch id in
+  vcs
+
+let checkout vcs name = { vcs with cur_branch = name }
+
+let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info }
+let get_info vcs id = Dag.get_info vcs.dag id
+
+let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i }
+let cluster_of vcs i = Dag.cluster_of vcs.dag i
+let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c }
+
+let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
+let dag vcs = vcs.dag
+
+let rec closure s d n =
+  let l = try Dag.from_node d n with Not_found -> [] in
+  List.fold_left (fun s (n',_) ->
+    if Dag.NodeSet.mem n' s then s
+    else closure s d n')
+  (Dag.NodeSet.add n s) l
+
+let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i
+
+let gc vcs =
+  let alive =
+    BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos)
+      vcs.heads Dag.NodeSet.empty in
+  let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in
+  { vcs with dag = Dag.del_nodes vcs.dag dead }, dead
+
+end
diff --git a/stm/vcs.mli b/stm/vcs.mli
new file mode 100644
index 000000000..6c3571a08
--- /dev/null
+++ b/stm/vcs.mli
@@ -0,0 +1,90 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This module builds a VCS like interface on top of Dag, used to build
+   a Dag instance by the State Transaction Machine.
+
+   This data structure does not hold system states:
+   - Edges are meant to hold a diff.
+     The delta between two states, or equivalent data like a vernac_expr whose
+     execution corresponds to the application of the diff.
+   - Nodes are empty, unless one adds explicit info.
+     The info could be a system state, obtaind by applying all the diffs
+     from the initial state, but is not necessarily there.
+   As a consequence, "checkout" just updates the current branch.
+
+   The type [id] is the type of commits (a node in the dag)
+   The type [Vcs.t] has 3 parameters:
+    ['info] data attached to a node (like a system state)
+    ['diff] data attached to an edge (the commit content, a "patch")
+    ['kind] extra data attached to a branch (like being the master branch)
+*)
+
+module type S = sig
+
+  module Branch :
+  sig
+    type t
+    val make : string -> t
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val to_string : t -> string
+    val master : t
+  end
+
+  type id
+  
+  type ('kind) branch_info = {
+    kind : [> `Master] as 'kind;
+    root : id;
+    pos  : id;
+  }
+  
+  type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
+  
+  val empty : id -> ('kind,'diff,'info) t
+  
+  val current_branch : ('k,'e,'i) t -> Branch.t
+  val branches : ('k,'e,'i) t -> Branch.t list
+  
+  val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
+  val branch :
+    ('kind,'e,'i) t -> ?root:id -> ?pos:id ->
+        Branch.t -> 'kind -> ('kind,'e,'i) t
+  val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+  val merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i) t
+  val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
+  val rewrite_merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+            Branch.t -> ('k,'diff,'i) t
+  val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+  
+  val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
+  val get_info : ('k,'e,'info) t -> id -> 'info option
+
+  module NodeSet : Set.S with type elt = id
+  
+  (* Removes all unreachable nodes and returns them *)
+  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+
+  val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+
+  (* read only dag *)
+  module Dag : Dag.S with type node = id
+  val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t
+ 
+  val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t
+  val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option
+  val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t 
+
+end
+
+module Make(OT : Map.OrderedType) : S with type id = OT.t
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
new file mode 100644
index 000000000..49cbcd246
--- /dev/null
+++ b/stm/vernac_classifier.ml
@@ -0,0 +1,189 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Errors
+open Pp
+
+let string_of_in_script b = if b then " (inside script)" else ""
+
+let string_of_vernac_type = function
+  | VtUnknown -> "Unknown"
+  | VtStartProof _ -> "StartProof"
+  | VtSideff _ -> "Sideff"
+  | VtQed VtKeep -> "Qed(keep)"
+  | VtQed VtDrop -> "Qed(drop)"
+  | VtProofStep -> "ProofStep"
+  | VtProofMode s -> "ProofMode " ^ s
+  | VtQuery b -> "Query" ^ string_of_in_script b
+  | 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
+
+let string_of_vernac_when = function
+  | VtLater -> "Later"
+  | VtNow -> "Now"
+
+let string_of_vernac_classification (t,w) =
+  string_of_vernac_type t ^ " " ^ string_of_vernac_when w
+
+let classifiers = ref []
+let declare_vernac_classifier
+  (s : string)
+  (f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
+=
+  classifiers := !classifiers @ [s,f]
+
+let elide_part_of_script_and_now (a, _) =
+  match a with
+  | VtQuery _ -> VtQuery false, VtNow
+  | VtStm (x, _) -> VtStm (x, false), VtNow
+  | x -> x, VtNow
+
+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
+    (* 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
+    | VernacTimeout (_,e) -> classify_vernac e
+    | VernacTime 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, VtNow
+        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+    (* Qed *)
+    | VernacEndProof Admitted | VernacAbort _ -> VtQed VtDrop, VtLater
+    | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
+    (* Query *)
+    | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
+    | VernacCheckMayEval _ -> VtQuery true, VtLater
+    (* ProofStep *)
+    | VernacProof _ 
+    | VernacBullet _ 
+    | VernacFocus _ | VernacUnfocus
+    | VernacSubproof _ | VernacEndSubproof 
+    | VernacSolve _ | VernacError _
+    | VernacCheckGuard
+    | VernacUnfocused
+    | VernacSolveExistential _ -> VtProofStep, VtLater
+    (* Options changing parser *)
+    | VernacUnsetOption (["Default";"Proof";"Using"])
+    | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
+    (* StartProof *)
+    | VernacDefinition (_,(_,i),ProveBody _) ->
+        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+    | VernacStartTheoremProof (_,l,_) ->
+        let ids = 
+          CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+    | VernacFixpoint (_,l) ->
+        let ids, open_proof =
+          List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+            id::l, b || p = None) ([],false) l in
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        else VtSideff ids, VtLater
+    | VernacCoFixpoint (_,l) ->
+        let ids, open_proof =
+          List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+            id::l, b || p = None) ([],false) l in
+        if open_proof then VtStartProof ("Classic",GuaranteesOpacity,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 snd 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] | _ -> []) @
+           CList.map_filter (function
+            | ((_,AssumExpr((_,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
+        VtSideff ids, VtLater
+    | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
+    | VernacBeginSection _
+    | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+    | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+    | VernacChdir _ 
+    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+    | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+    | VernacReserve _
+    | VernacGeneralizable _
+    | VernacSetOpacity _ | VernacSetStrategy _
+    | VernacUnsetOption _ | VernacSetOption _
+    | VernacAddOption _ | VernacRemoveOption _
+    | VernacMemOption _ | VernacPrintOption _
+    | VernacGlobalCheck _
+    | VernacDeclareReduction _
+    | VernacDeclareClass _ | VernacDeclareInstances _
+    | VernacRegister _
+    | VernacComments _ -> VtSideff [], VtLater
+    (* Who knows *)
+    | VernacList _
+    | VernacLoad _ -> VtSideff [], VtNow
+    (* (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,_,_) ->
+        VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+    | VernacDeclareModuleType ((_,id),bl,_,_) ->
+        VtSideff [id], if bl = [] then VtLater else VtNow
+    (* These commands alter the parser *)
+    | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
+    | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ 
+    | VernacSyntacticDefinition _
+    | VernacDeclareTacticDefinition _ | VernacTacticNotation _
+    | VernacRequire _ | VernacImport _ | VernacInclude _
+    | VernacDeclareMLModule _
+    | VernacContext _ (* TASSI: unsure *)
+    | VernacProofMode _ 
+    (* 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
+    (* What are these? *)
+    | VernacNop
+    | VernacToplevelControl _
+    | VernacRestoreState _
+    | VernacWriteState _ -> VtUnknown, 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 s)
+  in
+    static_classifier e
+
+let classify_as_query = VtQuery true, VtLater
+let classify_as_sideeff = VtSideff [], VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
new file mode 100644
index 000000000..bc0c0c2b3
--- /dev/null
+++ b/stm/vernac_classifier.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Genarg
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : vernac_expr -> vernac_classification
+
+(** Install a vernacular classifier for VernacExtend *)
+val declare_vernac_classifier :
+  string -> (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/vi_checking.ml b/stm/vi_checking.ml
new file mode 100644
index 000000000..cb6e60136
--- /dev/null
+++ b/stm/vi_checking.ml
@@ -0,0 +1,152 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+
+let check_vi (ts,f) =
+  Dumpglob.noglob ();
+  let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
+  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 
+  let add_timeout ~sec f =
+    ignore(Thread.create (fun () ->
+      while true do
+        Unix.sleep sec;
+        if not (f ()) then Thread.exit ()
+      done)
+    ())
+end)
+
+module IntOT = struct
+  type t = int
+  let compare = compare
+end
+
+module Pool = Map.Make(IntOT)
+
+let schedule_vi_checking j fs =
+  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  let jobs = ref [] in
+  List.iter (fun f ->
+    let f =
+      if Filename.check_suffix f ".vi" then Filename.chop_extension f
+      else f in
+    let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
+    Stm.set_compilation_hints long_f_dot_v;
+    let infos = Stm.info_tasks tasks in
+    let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
+    if infos <> [] then jobs := (f, eta, infos) :: !jobs)
+  fs;
+  let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
+  jobs := List.sort cmp_job !jobs;
+  let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in
+  let pool : Worker.process Pool.t ref = ref Pool.empty in
+  let rec filter_argv b = function
+    | [] -> []
+    | "-schedule-vi-checking" :: rest -> filter_argv true rest
+    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | _ :: rest when b -> filter_argv b rest
+    | s :: rest -> s :: filter_argv b rest in
+  let pack = function
+    | [] -> []
+    | ((f,_),_,_) :: _ as l ->
+        let rec aux last acc = function
+          | [] -> [last,acc]
+          | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
+          | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
+        aux f [] l in
+  let prog = Sys.argv.(0) in  
+  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let make_job () =
+    let cur = ref 0.0 in
+    let what = ref [] in
+    let j_left = j - Pool.cardinal !pool in
+    let take_next_file () =
+      let f, t, tasks = List.hd !jobs in
+      jobs := List.tl !jobs;
+      cur := !cur +. t;
+      what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in
+    if List.length !jobs >= j_left then take_next_file ()
+    else while !jobs <> [] &&
+         !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do
+      let f, t, tasks = List.hd !jobs in
+      jobs := List.tl !jobs;
+      let n, tt, id = List.hd tasks in
+      if List.length tasks > 1 then
+        jobs := (f, t -. tt, List.tl tasks) :: !jobs;
+      cur := !cur +. tt;
+      what := ((f,id),n,tt) :: !what;
+    done;
+    if !what = [] then take_next_file ();
+    eta := !eta -. !cur;
+    let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
+    List.flatten
+      (List.map (fun (f, tl) ->
+        "-check-vi-tasks" :: 
+        String.concat "," (List.map string_of_int tl) :: [f])
+      (pack (List.sort cmp_job !what))) in
+  let rc = ref 0 in
+  while !jobs <> [] || Pool.cardinal !pool > 0 do
+    while Pool.cardinal !pool < j && !jobs <> [] do
+      let args = Array.of_list (stdargs @ make_job ()) in
+      let proc, _, _ = Worker.spawn prog args in
+      pool := Pool.add (Worker.unixpid proc) proc !pool;
+    done;
+    let pid, ret = Unix.wait () in
+    if ret <> Unix.WEXITED 0 then rc := 1;
+    pool := Pool.remove pid !pool;
+  done;
+  exit !rc
+
+let schedule_vi_compilation j fs =
+  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  let jobs = ref [] in
+  List.iter (fun f ->
+    let f =
+      if Filename.check_suffix f ".vi" then Filename.chop_extension f
+      else f in
+    let paths = Loadpath.get_paths () in
+    let _, long_f_dot_v =
+      System.find_file_in_path ~warn:(Flags.is_verbose()) paths (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")
+      with Not_found -> 0.0 in
+    jobs := (f, eta) :: !jobs)
+  fs;
+  let cmp_job (_,t1) (_,t2) = compare t2 t1 in
+  jobs := List.sort cmp_job !jobs;
+  let pool : Worker.process Pool.t ref = ref Pool.empty in
+  let rec filter_argv b = function
+    | [] -> []
+    | "-schedule-vi2vo" :: rest -> filter_argv true rest
+    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | _ :: rest when b -> filter_argv b rest
+    | s :: rest -> s :: filter_argv b rest in
+  let prog = Sys.argv.(0) in  
+  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let make_job () =
+    let f, t = List.hd !jobs in
+    jobs := List.tl !jobs;
+    [ "-vi2vo"; f ] in
+  let rc = ref 0 in
+  while !jobs <> [] || Pool.cardinal !pool > 0 do
+    while Pool.cardinal !pool < j && !jobs <> [] do
+      let args = Array.of_list (stdargs @ make_job ()) in
+      let proc, _, _ = Worker.spawn prog args in
+      pool := Pool.add (Worker.unixpid proc) proc !pool;
+    done;
+    let pid, ret = Unix.wait () in
+    if ret <> Unix.WEXITED 0 then rc := 1;
+    pool := Pool.remove pid !pool;
+  done;
+  exit !rc
+
+  
diff --git a/stm/vi_checking.mli b/stm/vi_checking.mli
new file mode 100644
index 000000000..65414eda4
--- /dev/null
+++ b/stm/vi_checking.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* [check_vi tasks file] checks the [tasks] stored in [file] *)
+val check_vi : int list * string -> bool
+val schedule_vi_checking : int -> string list -> unit
+
+val schedule_vi_compilation : int -> string list -> unit
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
new file mode 100644
index 000000000..fcae4f20d
--- /dev/null
+++ b/stm/workerPool.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module Make(Worker : sig
+  type process
+  val spawn :
+      ?prefer_sock:bool -> ?env:string array -> string -> string array ->
+      process * in_channel * out_channel
+end) = struct
+
+type worker_id = int
+type spawn =
+  args:string array -> env:string array -> unit ->
+    in_channel * out_channel * Worker.process
+
+let slave_managers = ref None
+
+let n_workers () = match !slave_managers with
+  | None -> 0
+  | Some managers -> Array.length managers
+let is_empty () = !slave_managers = None
+
+let magic_no = 17
+
+let master_handshake worker_id ic oc =
+  try
+    Marshal.to_channel oc magic_no [];  flush oc;
+    let n = (Marshal.from_channel ic : int) in
+    if n <> magic_no then begin
+      Printf.eprintf "Handshake with %d failed: protocol mismatch\n" worker_id;
+      exit 1;
+    end
+  with e when Errors.noncritical e ->
+    Printf.eprintf "Handshake with %d failed: %s\n"
+      worker_id (Printexc.to_string e);
+    exit 1
+
+let respawn n ~args ~env () =
+  let proc, ic, oc = Worker.spawn ~env Sys.argv.(0) args in
+  master_handshake n ic oc;
+  ic, oc, proc
+
+let init ~size:n ~manager:manage_slave =
+  slave_managers := Some
+    (Array.init n (fun x ->
+       let cancel = ref false in
+       cancel, Thread.create (manage_slave ~cancel (x+1)) (respawn (x+1))))
+
+let cancel n =
+  match !slave_managers with
+  | None -> ()
+  | Some a ->
+      let switch, _ = a.(n) in
+      switch := true
+      
+let worker_handshake slave_ic slave_oc =
+  try
+    let v = (Marshal.from_channel slave_ic : int) in
+    if v <> magic_no then begin
+      prerr_endline "Handshake failed: protocol mismatch\n";
+      exit 1;
+    end;
+    Marshal.to_channel slave_oc v []; flush slave_oc;
+  with e when Errors.noncritical e ->
+    prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
+    exit 1
+
+end
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
new file mode 100644
index 000000000..d7a546929
--- /dev/null
+++ b/stm/workerPool.mli
@@ -0,0 +1,30 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module Make(Worker : sig
+  type process
+  val spawn :
+      ?prefer_sock:bool -> ?env:string array -> string -> string array ->
+      process * in_channel * out_channel
+end) : sig
+
+type worker_id = int
+type spawn =
+  args:string array -> env:string array -> unit ->
+    in_channel * out_channel * Worker.process
+
+val init :
+  size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) -> unit
+val is_empty : unit -> bool
+val n_workers : unit -> int
+val cancel : worker_id -> unit
+
+(* The worker should call this function *)
+val worker_handshake : in_channel -> out_channel -> unit
+
+end