Imported Upstream version 8.6upstream/8.6

19 files changed, 1391 insertions, 1436 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index cc973260..fa6422cd 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Pp
 open Util
 
@@ -60,9 +60,7 @@ module Make(T : Task) = struct
 
   type more_data =
     | MoreDataUnivLevel of Univ.universe_level list
- 
-  let request_expiry_of_task (t, c) = T.request_of_task t, c
-  
+
   let slave_respond (Request r) =
     let res = T.perform r in
     Response res
@@ -106,7 +104,8 @@ module Make(T : Task) = struct
       marshal_err ("unmarshal_more_data: "^s)
 
   let report_status ?(id = !Flags.async_proofs_worker_id) s =
-    Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
+    let open Feedback in
+    feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
 
   module Worker = Spawn.Sync(struct end)
 
@@ -125,7 +124,7 @@ module Make(T : Task) = struct
                  "-async-proofs-worker-priority";
                    Flags.string_of_priority !Flags.async_proofs_worker_priority]
         | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vi2vo"
+        | ("-async-proofs" |"-toploop" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -184,6 +183,13 @@ module Make(T : Task) = struct
         let () = Unix.sleep 1 in
         kill_if ()
     in
+    let kill_if () =
+      try kill_if ()
+      with Sys.Break ->
+        let () = stop_waiting := true in
+        let () = TQueue.broadcast queue in
+        Worker.kill proc
+    in
     let _ = Thread.create kill_if () in
 
     try while true do
@@ -223,10 +229,8 @@ module Make(T : Task) = struct
     | (Die | TQueue.BeingDestroyed) ->
         giveback_exec_token (); kill proc; exit ()
     | Sys_error _ | Invalid_argument _ | End_of_file ->
-        giveback_exec_token ();
         T.on_task_cancellation_or_expiration_or_slave_death !last_task;
-        kill proc;
-        exit ()
+        giveback_exec_token (); kill proc; exit ()
   end
 
   module Pool = WorkerPool.Make(Model)
@@ -294,11 +298,27 @@ module Make(T : Task) = struct
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
+  let pp_pid pp = 
+    (* Breaking all abstraction barriers... very nice *)
+    let get_xml pp = match Richpp.repr pp with
+      | Xml_datatype.Element("_", [], xml) -> xml
+      | _ -> assert false in
+    Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
+      get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
+      get_xml pp))
+
+  let debug_with_pid = Feedback.(function
+    | { contents = Message(Debug, loc, pp) } as fb ->
+       { fb with contents = Message(Debug,loc,pp_pid pp) }
+    | x -> x)
+
   let main_loop () =
+    (* We pass feedback to master *)
     let slave_feeder oc fb =
-      Marshal.to_channel oc (RespFeedback fb) []; flush oc in
-    Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Pp.log_via_feedback ();
+      Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
+    Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+    Feedback.set_logger Feedback.feedback_logger;
+    (* We ask master to allocate universe identifiers *)
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
@@ -314,7 +334,7 @@ module Make(T : Task) = struct
         let response = slave_respond request in
         report_status "Idle";
         marshal_response (Option.get !slave_oc) response;
-        Ephemeron.clear ()
+        CEphemeron.clear ()
       with
       | MarshalError s ->
         pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
@@ -337,7 +357,7 @@ module Make(T : Task) = struct
   let with_n_workers n f =
     let q = create n in 
     try let rc = f q in destroy q; rc
-    with e -> let e = Errors.push e in destroy q; iraise e
+    with e -> let e = CErrors.push e in destroy q; iraise e
 
   let n_workers { active } = Pool.n_workers active
 
diff --git a/stm/dag.ml b/stm/dag.ml
index 0c7f9f34..99e7c926 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -8,15 +8,6 @@
 
 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
 
@@ -31,45 +22,57 @@ module type S = sig
   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
 
+  module Property :
+  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
+    val having_it : 'd t -> NodeSet.t
+  end
+
+  val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+  val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+  val iter : ('e,'i,'d) t ->
+    (node -> 'd Property.t list -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
 end
 
 module Make(OT : Map.OrderedType) = struct
 
-module Cluster =
+module NodeSet = Set.Make(OT)
+
+module Property =
 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
+  type 'd t = { data : 'd; uid : int; having_it : NodeSet.t }
+  let equal { uid = i1 } { uid = i2 } = Int.equal i1 i2
+  let compare { uid = i1 } { uid = i2 } = Int.compare i1 i2
+  let to_string { uid = i } = string_of_int i
+  let data { data = d } = d
+  let having_it { having_it } = having_it
 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;
+  properties : 'data Property.t list NodeMap.t;
   infos : 'info NodeMap.t;
 }
 
 let empty = {
   graph = NodeMap.empty;
-  clusters = NodeMap.empty;
+  properties = NodeMap.empty;
   infos = NodeMap.empty;
 }
 
@@ -94,7 +97,7 @@ let del_edge dag id tgt = { dag with
 
 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;
+  properties = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.properties;
   graph = NodeMap.filter (fun n l ->
       let drop = NodeSet.mem n s in
       if not drop then
@@ -102,20 +105,31 @@ let del_nodes dag s = {
       not drop)
     dag.graph }
 
+let map_add_list k v m =
+  try
+    let l = NodeMap.find k m in
+    NodeMap.add k (v::l) m
+  with Not_found -> NodeMap.add k [v] m
+
 let clid = ref 1
-let create_cluster dag l data =
+let create_property 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 having_it = List.fold_right NodeSet.add l NodeSet.empty in
+  let property = { Property.data; uid = !clid; having_it } in
+  { dag with properties =
+     List.fold_right (fun x ps -> map_add_list x property ps) l dag.properties }
+
+let property_of dag id =
+  try NodeMap.find id dag.properties
+  with Not_found -> []
+
+let del_property dag c =
+  { dag with properties =
+     NodeMap.filter (fun _ cl -> cl <> [])
+       (NodeMap.map (fun cl ->
+          List.filter (fun c' ->
+            not (Property.equal c' c)) cl)
+          dag.properties) }
 
 let get_info dag id =
   try Some (NodeMap.find id dag.infos)
@@ -126,7 +140,7 @@ 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
+  NodeMap.iter (fun k v -> f k (property_of dag k) (get_info dag k) v) dag.graph
 
 let all_nodes dag = NodeMap.domain dag.graph
 
diff --git a/stm/dag.mli b/stm/dag.mli
index 6b4442df..e783cd8e 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -7,19 +7,7 @@
 (************************************************************************)
 
 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
 
@@ -34,19 +22,35 @@ module type S = sig
   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
+  (* A property applies to a set of nodes and holds some data.
+     Stm uses this feature to group nodes contributing to the same proofs and
+     to structure proofs in boxes limiting the scope of errors *)
+  module Property :
+  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
+    val having_it : 'd t -> NodeSet.t
+  end
+
+  val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+  val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+  val iter : ('e,'i,'d) t -> 
+    (node -> 'd Property.t list -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
+  end
 
-module Make(OT : Map.OrderedType) : S with type node = OT.t
+module Make(OT : Map.OrderedType) : S
+with type node = OT.t
+and type NodeSet.t = Set.Make(OT).t
+and type NodeSet.elt = OT.t
 
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f06abfcc..022c89ad 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -9,7 +9,7 @@
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
 
-open Errors
+open CErrors
 open Util
 open Flags
 open Pp
@@ -31,20 +31,22 @@ open Reductionops
 open Constrexpr
 open Constrintern
 open Impargs
+open Context.Rel.Declaration
 
 type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
   try hook l c
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     iraise (fix_exn e)
 
 (* Support for mutually proved theorems *)
 
 let retrieve_first_recthm = function
   | VarRef id ->
-      (pi2 (Global.lookup_named id),variable_opacity id)
+      let open Context.Named.Declaration in
+      (get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
       (Global.body_of_constant_body cb, is_opaque cb)
@@ -77,7 +79,7 @@ let adjust_guardness_conditions const = function
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                 env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
-	        search_guard Loc.ghost env
+                search_guard Loc.ghost env
                   possible_indexes fixdecls in
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
@@ -104,20 +106,21 @@ let find_mutually_recursive_statements thms =
       (* 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))
+        (fun env c -> fst (whd_all_stack env Evd.empty c))
         (Global.env()) hyps in
       let ind_hyps =
-        List.flatten (List.map_i (fun i (_,b,t) ->
+        List.flatten (List.map_i (fun i decl ->
+          let t = get_type decl in
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
               [ind,x,i]
           | _ ->
               []) 0 (List.rev whnf_hyp_hds)) in
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
-        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+        let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
         match kind_of_term whnf_ccl with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
@@ -147,7 +150,7 @@ let find_mutually_recursive_statements thms =
 	  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.");
+	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
 	  flush_all ();
           indccl, true, []
       | [], _::_ ->
@@ -155,7 +158,7 @@ let find_mutually_recursive_statements thms =
           | ind :: _ ->
             if List.distinct_f ind_ord (List.map pi1 ind)
             then
-              if_verbose msg_info
+              if_verbose Feedback.msg_info
                 (strbrk
                    ("Coinductive statements do not follow the order of "^
                     "definition, assuming the proof to be by induction."));
@@ -207,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
     definition_message id;
     Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     iraise (fix_exn e)
 
 let default_thm_id = Id.of_string "Unnamed_thm"
@@ -249,10 +252,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
   | Some body ->
       let body = norm body in
       let k = Kindops.logical_kind_of_goal_kind kind in
-      let body_i = match kind_of_term body with
+      let rec body_i t = match kind_of_term t with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
+        | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
+        | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
+        | App (t, args) -> mkApp (body_i t, args)
         | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
+      let body_i = body_i body in
       match locality with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
@@ -298,13 +305,16 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident =
 
 (* Admitted *)
 
+let warn_let_as_axiom =
+  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
+                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
+                                spc () ++ strbrk "declared as an axiom.")
+
 let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ ->
-    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
-      str "declared as an axiom.")
+  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
   Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
@@ -329,10 +339,11 @@ let check_exist =
   )
 
 let universe_proof_terminator compute_guard hook =
-  let open Proof_global in function
+  let open Proof_global in
+  make_terminator begin function
   | Admitted (id,k,pe,(ctx,pl)) ->
       admit (id,k,pe) pl (hook (Some ctx)) ();
-      Pp.feedback Feedback.AddedAxiom
+      Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
         | Vernacexpr.Transparent -> false, true, []
@@ -347,12 +358,16 @@ let universe_proof_terminator compute_guard hook =
           save_anonymous_with_strength ~export_seff proof kind id
       end;
       check_exist exports
+  end
 
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
 
-let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = standard_proof_terminator compute_guard hook in
+let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = match terminator with
+  | None -> standard_proof_terminator compute_guard hook
+  | Some terminator -> terminator compute_guard hook
+  in
   let sign = 
     match sign with
     | Some sign -> sign
@@ -361,8 +376,11 @@ let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   !start_hook c;
   Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
-  let terminator = universe_proof_terminator compute_guard hook in
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = match terminator with
+  | None -> universe_proof_terminator compute_guard hook
+  | Some terminator -> terminator compute_guard hook
+  in
   let sign = 
     match sign with
     | Some sign -> sign
@@ -392,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
     | 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
+      let rec_tac = rec_tac_initializer finite guard thms snl in
       Some (match init_tac with
         | None -> 
             if Flags.is_auto_intros () then 
@@ -422,7 +440,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
+	    let ctx = UState.context_set (*FIXME*) ctx in
 	    let body = Option.map norm body in
             List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
@@ -431,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
       start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
-let start_proof_com kind thms hook =
+let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
   let levels = Option.map snd (fst (List.hd thms)) in 
   let evdref = ref (match levels with
@@ -441,8 +459,10 @@ let start_proof_com kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
-    let ids = List.map pi1 ctx in
+    let flags = all_and_fail_flags in
+    let flags = { flags with use_hook = inference_hook } in
+    evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
+    let ids = List.map get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
@@ -451,6 +471,11 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+  let () =
+    match levels with
+    | None -> ()
+    | Some l -> ignore (Evd.universe_context evd ?names:l)
+  in
   let evd =
     if pi2 kind then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
@@ -461,6 +486,18 @@ let start_proof_com kind thms hook =
 
 (* Saving a proof *)
 
+let keep_admitted_vars = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "keep section variables in admitted proofs";
+      optkey   = ["Keep"; "Admitted"; "Variables"];
+      optread  = (fun () -> !keep_admitted_vars);
+      optwrite = (fun b -> keep_admitted_vars := b) }
+
 let save_proof ?proof = function
   | Vernacexpr.Admitted ->
       let pe =
@@ -474,14 +511,18 @@ let save_proof ?proof = function
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context (fst universes) in
-            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
+            let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
+            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
         | None ->
+            let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
+            let universes = Proof.initial_euctx pftree in
             (* This will warn if the proof is complete *)
-            let pproofs, universes =
+            let pproofs, _univs =
               Proof_global.return_proof ~allow_partial:true () in
             let sec_vars =
-              match  Pfedit.get_used_variables(), pproofs with
+              if not !keep_admitted_vars then None
+              else match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
               | None, (pproof, _) :: _ -> 
                   let env = Global.env () in
@@ -490,11 +531,12 @@ let save_proof ?proof = function
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
 	    let names = Pfedit.get_universe_binders () in
-            let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+            let evd = Evd.from_ctx universes in
+            let binders, ctx = Evd.universe_context ?names evd in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
 		     (universes, Some binders))
       in
-      Proof_global.get_terminator() pe
+      Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
@@ -504,12 +546,10 @@ let save_proof ?proof = function
       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))
+      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    let env = Global.env () in
-    (Evd.from_env env, env)
+  Pfedit.get_current_context ()
+           
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 16e54e31..39c089be 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -9,8 +9,6 @@
 open Names
 open Term
 open Decl_kinds
-open Constrexpr
-open Vernacexpr
 open Pfedit
 
 type 'a declaration_hook
@@ -24,16 +22,20 @@ val call_hook :
 val set_start_hook : (types -> unit) -> unit
 
 val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
-val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
+val start_proof_com :
+  ?inference_hook:Pretyping.inference_hook ->
+  goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
@@ -43,6 +45,11 @@ val start_proof_with_initialization :
      (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
+val universe_proof_terminator :
+  Proof_global.lemma_possible_guards ->
+    (Evd.evar_universe_context option -> unit declaration_hook) ->
+    Proof_global.proof_terminator
+
 val standard_proof_terminator :
   Proof_global.lemma_possible_guards -> unit declaration_hook ->
     Proof_global.proof_terminator
@@ -60,4 +67,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
-
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
new file mode 100644
index 00000000..8162fc3b
--- /dev/null
+++ b/stm/proofBlockDelimiter.ml
@@ -0,0 +1,184 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Stm
+
+module Util : sig
+
+val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+val crawl :
+  document_view -> ?init:document_node option ->
+  ('a -> document_node -> 'a until) -> 'a ->
+    static_block_declaration option
+
+val unit_val : Stm.DynBlockData.t
+val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
+val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
+
+end = struct
+
+let unit_tag = DynBlockData.create "unit"
+let unit_val = DynBlockData.Easy.inj () unit_tag
+
+let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
+let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
+
+let simple_goal sigma g gs =
+  let open Evar in
+  let open Evd in
+  let open Evarutil in
+  let evi = Evd.find sigma g in
+  Set.is_empty (evars_of_term evi.evar_concl) &&
+  Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+  not (List.exists (Proofview.depends_on sigma g) gs)
+
+let is_focused_goal_simple id =
+  match state_of_id id with
+  | `Expired | `Error _ | `Valid None -> `Not
+  | `Valid (Some { proof }) ->
+       let proof = Proof_global.proof_of_state proof in
+       let focused, r1, r2, r3, sigma = Proof.proof proof in
+       let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+       if List.for_all (fun x -> simple_goal sigma x rest) focused
+       then `Simple focused
+       else `Not
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
+  let rec crawl node acc =
+    match node with
+    | None -> None
+    | Some node ->
+        match f acc node with
+        | `Stop -> None
+        | `Found x -> Some x
+        | `Cont acc -> crawl (prev_node node) acc in
+  crawl init acc
+
+end
+
+include Util
+
+(* ****************** - foo - bar - baz *********************************** *)
+
+let static_bullet ({ entry_point; prev_node } as view) =
+  match entry_point.ast with
+  | Vernacexpr.VernacBullet b ->
+      let base = entry_point.indentation in
+      let last_tac = prev_node entry_point in
+      crawl view ~init:last_tac (fun prev node ->
+        if node.indentation < base then `Stop else
+        if node.indentation > base then `Cont node else
+        match node.ast with
+        | Vernacexpr.VernacBullet b' when b = b' ->
+          `Found { block_stop = entry_point.id; block_start = prev.id;
+                   dynamic_switch = node.id; carry_on_data = of_bullet_val b }
+        | _ -> `Stop) entry_point
+  | _ -> assert false
+
+let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+  "bullet" static_bullet dynamic_bullet
+
+(* ******************** { block } ***************************************** *)
+  
+let static_curly_brace ({ entry_point; prev_node } as view) =
+  assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+  crawl view (fun (nesting,prev) node ->
+    match node.ast with
+    | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+      `Found { block_stop = entry_point.id; block_start = prev.id;
+               dynamic_switch = node.id; carry_on_data = unit_val }
+    | Vernacexpr.VernacSubproof _ ->
+      `Cont (nesting - 1,node)
+    | Vernacexpr.VernacEndSubproof ->
+      `Cont (nesting + 1,node)
+    | _ -> `Cont (nesting,node)) (-1, entry_point)
+
+let dynamic_curly_brace { dynamic_switch = id } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = Some Vernacexpr.VernacEndSubproof
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+  "curly" static_curly_brace dynamic_curly_brace
+
+(* ***************** par: ************************************************* *)
+
+let static_par { entry_point; prev_node } =
+  match prev_node entry_point with
+  | None -> None
+  | Some { id = pid } ->
+      Some { block_stop = entry_point.id; block_start = pid;
+             dynamic_switch = pid; carry_on_data = unit_val }
+
+let dynamic_par { dynamic_switch = id } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = None;
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "par" static_par dynamic_par
+
+(* ***************** simple indentation *********************************** *)
+
+let static_indent ({ entry_point; prev_node } as view) =
+   Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id);
+   match prev_node entry_point with
+   | None -> None
+   | Some last_tac ->
+      if last_tac.indentation <= entry_point.indentation then None
+      else
+        crawl view ~init:(Some last_tac) (fun prev node ->
+        if node.indentation >= last_tac.indentation then `Cont node
+        else 
+          `Found { block_stop = entry_point.id; block_start = node.id;
+                   dynamic_switch = node.id;
+                   carry_on_data = of_vernac_expr_val entry_point.ast }
+        ) last_tac
+
+let dynamic_indent { dynamic_switch = id; carry_on_data = e } =
+  Printf.eprintf "%s\n" (Stateid.to_string id);
+  match is_focused_goal_simple id with
+  | `Simple [] -> `Leaks
+  | `Simple focused ->
+      let but_last = List.tl (List.rev focused) in 
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = but_last;
+         recovery_command = Some (to_vernac_expr_val e);
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "indent" static_indent dynamic_indent
+
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
new file mode 100644
index 00000000..a55032a4
--- /dev/null
+++ b/stm/proofBlockDelimiter.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file implements proof block detection for:
+   - blocks delimited by { and }
+   - bullets with indentation
+   - par: terminator
+
+   It exports utility functions to ease the development of other proof block
+   detection code.
+*)
+
+(** A goal is simple if it nor depends on nor impacts on any other goal.
+    This function is used to detect, dynamically, if a proof block leaks,
+    i.e. if skipping it could impact other goals (like not instantiating their
+    type).  `Simple carries the list of focused goals.
+*)
+val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
+
+(* Simpler function to crawl the document backward to detect the block.
+ * ?init is the entry point of the document view if not given *)
+val crawl :
+  Stm.document_view -> ?init:Stm.document_node option ->
+  ('a -> Stm.document_node -> 'a until) -> 'a ->
+    Stm.static_block_declaration option
+
+(* Dummy value for static_block_declaration when no real value is needed *)
+val unit_val : Stm.DynBlockData.t
+
+(* Bullets *)
+val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+
diff --git a/stm/spawned.ml b/stm/spawned.ml
index c6df8726..c5bd5f6f 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
 
 type chandescr = AnonPipe | Socket of string * int * 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 pr pw =
   let open Unix in
   let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
@@ -59,7 +46,7 @@ let control_channel = ref None
 let channels = ref None
 
 let init_channels () =
-  if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
+  if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice");
   let () = match !main_channel with
   | None -> ()
   | Some (Socket(mh,mpr,mpw)) ->
@@ -78,7 +65,7 @@ let init_channels () =
   | Some (Socket (ch, cpr, cpw)) ->
     controller ch cpr cpw
   | Some AnonPipe ->
-    Errors.anomaly (Pp.str "control channel cannot be a pipe")
+    CErrors.anomaly (Pp.str "control channel cannot be a pipe")
 
 let get_channels () =
   match !channels with
diff --git a/stm/stm.ml b/stm/stm.ml
index d8b2de4a..b4331dc4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -8,16 +8,21 @@
 
 let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
 
-let prerr_endline s = if false then begin pr_err s end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if false then begin pr_err (s ()) end else ()
+let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+
+(* Opening ppvernac below aliases Richpp, see PR#185 *)
+let pp_to_richpp  = Richpp.richpp_of_pp
+let str_to_richpp = Richpp.richpp_of_string
 
 open Vernacexpr
-open Errors
+open CErrors
 open Pp
 open Names
 open Util
 open Ppvernac
 open Vernac_classifier
+open Feedback
 
 module Hooks = struct
 
@@ -27,28 +32,25 @@ let with_fail, with_fail_hook = Hook.make ()
 
 let state_computed, state_computed_hook = Hook.make
  ~default:(fun state_id ~in_cache ->
-    feedback ~state_id Feedback.Processed) ()
+    feedback ~id:(State state_id) Processed) ()
 
 let state_ready, state_ready_hook = Hook.make
  ~default:(fun state_id -> ()) ()
 
-let forward_feedback, forward_feedback_hook = Hook.make
- ~default:(function
-    | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
-          feedback ~edit_id ~route contents
-    | { Feedback.id = Feedback.State state_id; route; contents } ->
-          feedback ~state_id ~route contents) ()
+let forward_feedback, forward_feedback_hook = 
+  let m = Mutex.create () in
+  Hook.make ~default:(function
+    | { id = id; route; contents } ->
+        try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
+        with e -> Mutex.unlock m; raise e) ()
 
 let parse_error, parse_error_hook = Hook.make
- ~default:(function
-    | Feedback.Edit edit_id -> fun loc msg ->
-        feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
-    | Feedback.State state_id -> fun loc msg ->
-        feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ ~default:(fun id loc msg ->
+        feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
 
 let execution_error, execution_error_hook = Hook.make
  ~default:(fun state_id loc msg ->
-    feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+    feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
@@ -80,8 +82,28 @@ let interactive () =
 
 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
+type aast = {
+  verbose : bool;
+  loc : Loc.t;
+  indentation : int;
+  strlen : int;
+  mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
+}
+let pr_ast { expr; indentation } = int indentation ++ str " " ++ pr_vernac expr
+
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
+(* Commands piercing opaque *)
+let may_pierce_opaque = function
+  | { expr = VernacPrint _ } -> true
+  | { expr = VernacExtend (("Extraction",_), _) } -> true
+  | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
+  | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+  | _ -> false
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 let vernac_interp ?proof id ?route { verbose; loc; expr } =
@@ -89,34 +111,48 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
     | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
+    | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
     | _ -> false in
   if internal_command expr then begin
-    prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
+    prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
   end else begin
-    set_id_for_feedback ?route (Feedback.State id);
+    set_id_for_feedback ?route (State id);
     Aux_file.record_in_aux_set_at loc;
-    prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
+    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
     try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
     with e ->
-      let e = Errors.push e in
+      let e = CErrors.push e in
       iraise Hooks.(call_process_error_once e)
   end
 
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let vernac_parse ?newtip ?route eid s =
+let indentation_of_string s =
+  let len = String.length s in
+  let rec aux n i precise =
+    if i >= len then 0, precise, len
+    else
+      match s.[i] with
+      | ' ' | '\t' -> aux (succ n) (succ i) precise
+      | '\n' | '\r' -> aux 0 (succ i) true
+      | _ -> n, precise, len in
+  aux 0 0 false
+
+let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
   let feedback_id = 
-    if Option.is_empty newtip then Feedback.Edit eid
-    else Feedback.State (Option.get newtip) in
+    if Option.is_empty newtip then Edit eid
+    else State (Option.get newtip) in
+  let indentation, precise, strlen = indentation_of_string s in
+  let indentation =
+    if precise then indentation else indlen_prev () + indentation in
   set_id_for_feedback ?route feedback_id;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   Flags.with_option Flags.we_are_parsing (fun () ->
     try
       match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
       | None -> raise (Invalid_argument "vernac_parse")
-      | Some ast -> ast
-    with e when Errors.noncritical e ->
-      let (e, info) = Errors.push e in
+      | Some (loc, ast) -> indentation, strlen, loc, ast
+    with e when CErrors.noncritical e ->
+      let (e, info) = CErrors.push e in
       let loc = Option.default Loc.ghost (Loc.get_loc info) in
       Hooks.(call parse_error feedback_id loc (iprint (e, info)));
       iraise (e, info))
@@ -124,13 +160,13 @@ let vernac_parse ?newtip ?route eid s =
 
 let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
-  with Proof_global.NoCurrentProof -> str""
+  with Proof_global.NoCurrentProof -> Pp.str ""
 
 let update_global_env () =
   if Proof_global.there_are_pending_proofs () then
     Proof_global.update_global_env ()
 
-module Vcs_ = Vcs.Make(Stateid)
+module Vcs_ = Vcs.Make(Stateid.Self)
 type future_proof = Proof_global.closed_proof_output Future.computation
 type proof_mode = string
 type depth = int
@@ -140,22 +176,27 @@ type branch_type =
   | `Proof of proof_mode * depth
   | `Edit of
       proof_mode * Stateid.t * Stateid.t  * vernac_qed_type * Vcs_.Branch.t ]
+(* TODO 8.7 : split commands and tactics, since this type is too messy now *)
 type cmd_t = {
-  ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
-  ceff : bool; (* is a side-effecting command *)
-  cast : ast;
+  ctac : bool; (* is a tactic *)
+  ceff : bool; (* is a side-effecting command in the middle of a proof *)
+  cast : aast;
   cids : Id.t list;
-  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
-type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+  cblock : proof_block_name option;
+  cqueue : [ `MainQueue
+           | `TacQueue of solving_tac * anon_abstracting_tac * cancel_switch
+           | `QueryQueue of cancel_switch
+           | `SkipQueue ] }
+type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
 type qed_t = {
-  qast : ast;
+  qast : aast;
   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 * ast
+type seff_t = aast option
+type alias_t = Stateid.t * aast
 type transaction =
   | Cmd    of cmd_t
   | Fork   of fork_t
@@ -167,40 +208,69 @@ type step =
   [ `Cmd    of cmd_t
   | `Fork   of fork_t * Stateid.t option
   | `Qed    of qed_t * Stateid.t
-  | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ]
+  | `Sideff of [ `Ast of aast * Stateid.t | `Id of Stateid.t ]
   | `Alias  of alias_t ]
 type visit = { step : step; next : Stateid.t }
 
+let mkTransTac cast cblock cqueue =
+  Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false }
+let mkTransCmd cast cids ceff cqueue =
+  Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
 
 (* Parts of the system state that are morally part of the proof state *)
 let summary_pstate = [ Evarutil.meta_counter_summary_name;
-                       Evarutil.evar_counter_summary_name;
+                       Evd.evar_counter_summary_name;
                        "program-tcc-table" ]
-type state = {
-  system : States.state;
-  proof : Proof_global.state;
-  shallow : bool
+type cached_state =
+  | Empty
+  | Error of Exninfo.iexn
+  | Valid of state
+and state = { (* TODO: inline records in OCaml 4.03 *)
+  system : States.state;       (* summary + libstack *)
+  proof : Proof_global.state;  (* proof state *)
+  shallow : bool               (* is the state trimmed down (libstack) *)
 }
 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;
+type 'vcs state_info = { (* TODO: Make this record private to VCS *)
+  mutable n_reached : int;      (* debug cache: how many times was computed *)
+  mutable n_goals : int;        (* open goals: indentation *)
+  mutable state : cached_state; (* state value *)
   mutable vcs_backup : 'vcs option * backup option;
 }
 let default_info () =
-  { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None }
+  { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
+
+module DynBlockData : Dyn.S = Dyn.Make(struct end)
+
+(* Clusters of nodes implemented as Dag properties.  While Dag and Vcs impose
+ * no constraint on properties, here we impose boxes to be non overlapping.
+ * Such invariant makes sense for the current kinds of boxes (proof blocks and
+ * entire proofs) but may make no sense and dropped/refined in the future.
+ * Such invariant is useful to detect broken proof block detection code *)
+type box =
+  | ProofTask of pt
+  | ProofBlock of static_block_declaration * proof_block_name
+and pt = { (* TODO: inline records in OCaml 4.03 *)
+  lemma : Stateid.t;
+  qed   : Stateid.t;
+}
+and static_block_declaration = {
+  block_start : Stateid.t;
+  block_stop  : Stateid.t;
+  dynamic_switch : Stateid.t;
+  carry_on_data : DynBlockData.t;
+}
 
 (* 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 proof_nesting : (branch_type, 't,'i,'c) Vcs_.t -> int
   val find_proof_at_depth :
-    (branch_type, 't, 'i) Vcs_.t -> int ->
+          (branch_type, 't, 'i,'c) 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
+  val visit : (branch_type, transaction,'i,'c) Vcs_.t -> Vcs_.Dag.node -> visit
 
 end = struct (* {{{ *)
 
@@ -216,7 +286,7 @@ end = struct (* {{{ *)
   let find_proof_at_depth vcs pl =
     try List.find (function
           | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
-          | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
+          | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
           | _ -> false)
         (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
     with Not_found -> failwith "find_proof_at_depth"
@@ -224,9 +294,9 @@ end = struct (* {{{ *)
   exception Expired
   let visit vcs id =
     if Stateid.equal id Stateid.initial then
-      anomaly(str"Visiting the initial state id")
+      anomaly(Pp.str "Visiting the initial state id")
     else if Stateid.equal id Stateid.dummy then
-      anomaly(str"Visiting the dummy state id")
+      anomaly(Pp.str "Visiting the dummy state id")
     else
     try
       match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -242,7 +312,7 @@ end = struct (* {{{ *)
       | [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))
+      | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
     with Not_found -> raise Expired
 
 end (* }}} *)
@@ -264,7 +334,7 @@ module VCS : sig
     pos  : id;
   }
 
-  type vcs = (branch_type, transaction, vcs state_info) Vcs_.t
+  type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
 
   val init : id -> unit
 
@@ -278,30 +348,32 @@ module VCS : sig
   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 mk_branch_name : aast -> 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 reachable : id -> Stateid.Set.t
   val cur_tip : unit -> id
 
   val get_info : id -> vcs state_info
-  val reached : id -> bool -> unit
+  val reached : id -> unit
   val goals : id -> int -> unit
-  val set_state : id -> state -> unit
-  val get_state : id -> state option
+  val set_state : id -> cached_state -> unit
+  val get_state : id -> cached_state
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
-  val slice : start:id -> stop:id -> vcs
-  val nodes_in_slice : start:id -> stop:id -> Stateid.t list
+  val slice : block_start:id -> block_stop:id -> vcs
+  val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list
   
-  val create_cluster : id list -> qed:id -> start:id -> unit
-  val cluster_of : id -> (id * id) option
-  val delete_cluster_of : id -> unit
+  val create_proof_task_box : id list -> qed:id -> block_start:id -> unit
+  val create_proof_block : static_block_declaration -> string -> unit
+  val box_of : id -> box list
+  val delete_boxes_of : id -> unit
+  val proof_task_box_of : id -> pt option
 
   val proof_nesting : unit -> int
   val checkout_shallowest_proof_branch : unit -> unit
-  val propagate_sideff : ast option -> unit
+  val propagate_sideff : replay:aast option -> unit
 
   val gc : unit -> unit
 
@@ -317,7 +389,6 @@ end = struct (* {{{ *)
   include Vcs_
   exception Expired = Vcs_aux.Expired
 
-  module StateidSet = Set.Make(Stateid)
   open Printf
 
   let print_dag vcs () =
@@ -325,21 +396,21 @@ end = struct (* {{{ *)
       "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
     let string_of_transaction = function
       | Cmd { cast = t } | Fork (t, _,_,_) ->
-          (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+          (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff (Some t) ->
           sprintf "Sideff(%s)"
-            (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+            (try Pp.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
+      | Some { state = Valid _ } -> true
       | _ -> false in
     let is_red id =
       match get_info vcs id with
-      | Some s -> Int.equal s.n_reached ~-1
+      | Some { state = Error _ } -> true
       | _ -> false in
     let head = current_branch vcs in
     let heads =
@@ -359,8 +430,6 @@ end = struct (* {{{ *)
     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 -> ""
@@ -373,39 +442,71 @@ end = struct (* {{{ *)
     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 ids = ref Stateid.Set.empty in
+    let boxes = ref [] in
+    (* Fill in *)
+    Dag.iter graph (fun from _ _ l ->
+      ids := Stateid.Set.add from !ids;
+      List.iter (fun box -> boxes := box :: !boxes)
+        (Dag.property_of graph from);
+      List.iter (fun (dest, _) ->
+        ids := Stateid.Set.add dest !ids;
+        List.iter (fun box -> boxes := box :: !boxes)
+          (Dag.property_of graph dest))
+      l);
+    boxes := CList.sort_uniquize Dag.Property.compare !boxes;
+
     let oc = open_out fname_dot in
     output_string oc "digraph states {\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 [xlabel=%s,labelfloat=%b];\n"
-           (node from) (node dest) (edge trans) (c1 && c2)) l
+       fprintf oc "%s -> %s [xlabel=%s,labelfloat=true];\n"
+           (node from) (node dest) (edge trans)) 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;
+
+    let contains b1 b2 =
+      Stateid.Set.subset
+        (Dag.Property.having_it b2) (Dag.Property.having_it b1) in
+    let same_box = Dag.Property.equal in
+    let outerboxes boxes =
+       List.filter (fun b ->
+         not (List.exists (fun b1 ->
+           not (same_box b1 b) && contains b1 b) boxes)           
+         ) boxes in
+    let rec rec_print b =
+      boxes := CList.remove same_box b !boxes;
+      let sub_boxes = List.filter (contains b) (outerboxes !boxes) in
+      fprintf oc "subgraph cluster_%s {\n" (Dag.Property.to_string b);
+      List.iter rec_print sub_boxes;
+      Stateid.Set.iter (fun id ->
+        if Stateid.Set.mem id !ids then begin
+          ids := Stateid.Set.remove id !ids;
+          nodefmt oc id
+        end)
+        (Dag.Property.having_it b);
+      match Dag.Property.data b with
+      | ProofBlock ({ dynamic_switch = id }, lbl) ->
+          fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id);
+          fprintf oc "color=red; }\n"
+      | ProofTask _ -> fprintf oc "color=blue; }\n"
+      in
+    List.iter rec_print (outerboxes !boxes);
+    Stateid.Set.iter (nodefmt oc) !ids;
+
     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
+  type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
   let init id =
@@ -442,13 +543,12 @@ end = struct (* {{{ *)
     | Some x -> x
     | None -> raise Vcs_aux.Expired
   let set_state id s =
-    (get_info id).state <- Some s;
+    (get_info id).state <- s;
     if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
   let get_state id = (get_info id).state
-  let reached id b =
+  let reached id =
     let info = get_info id in
-    if b then info.n_reached <- info.n_reached + 1
-    else info.n_reached <- -1
+    info.n_reached <- info.n_reached + 1
   let goals id n = (get_info id).n_goals <- n
   let cur_tip () = get_branch_pos (current_branch ())
 
@@ -466,14 +566,14 @@ end = struct (* {{{ *)
         let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
-        prerr_endline ("mode:" ^ mode);
+        prerr_endline (fun () -> "mode:" ^ mode);
         Proof_global.activate_proof_mode mode
       with Failure _ ->
         checkout Branch.master;
-        Proof_global.disactivate_proof_mode "Classic"
+        Proof_global.disactivate_current_proof_mode ()
 
   (* copies the transaction on every open branch *)
-  let propagate_sideff t =
+  let propagate_sideff ~replay:t =
     List.iter (fun b ->
       checkout b;
       let id = new_node () in
@@ -482,54 +582,91 @@ end = struct (* {{{ *)
   
   let visit id = Vcs_aux.visit !vcs id
 
-  let nodes_in_slice ~start ~stop =
+  let nodes_in_slice ~block_start ~block_stop =
     let rec aux id =
-      if Stateid.equal id start then [] else
+      if Stateid.equal id block_start 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 stop
+      | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^
+                         " to "^Stateid.to_string block_stop))
+    in aux block_stop
 
-  let slice ~start ~stop =
-    let l = nodes_in_slice ~start ~stop in
+  let slice ~block_start ~block_stop =
+    let l = nodes_in_slice ~block_start ~block_stop in
     let copy_info v id =
       Vcs_.set_info v id
-        { (get_info id) with state = None; vcs_backup = None,None } in
+        { (get_info id) with state = Empty; 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 start in
-    let v = copy_info v start in
+    let copy_proof_blockes v =
+      let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
+      let props =
+        Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in
+      let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in
+      List.fold_left (fun v p ->
+        Vcs_.create_property v
+          (Stateid.Set.elements (Vcs_.Dag.Property.having_it p))
+          (Vcs_.Dag.Property.data p)) v props
+    in
+    let v = Vcs_.empty block_start in
+    let v = copy_info v block_start 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 start).state));
+    assert (match (get_info block_start).state with Valid _ -> true | _ -> false);
     (* 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 stop
-
-  let nodes_in_slice ~start ~stop =
-    List.rev (List.map fst (nodes_in_slice ~start ~stop))
-
-  let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start)
-  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)
+      match (get_info id).state with
+      | Empty | Error _ -> fill (Vcs_aux.visit v id).next
+      | Valid _ -> copy_info_w_state v id in
+    let v = fill block_stop in
+    (* We put in the new dag the first state (since Qed shall run on it,
+     * see check_task_aux) *)
+    let v = copy_info_w_state v block_start in
+    copy_proof_blockes v
+
+  let nodes_in_slice ~block_start ~block_stop =
+    List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop))
+
+  let topo_invariant l =
+    let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in
+    List.for_all
+      (fun x ->
+         let props = property_of !vcs x in
+         let sets = List.map Dag.Property.having_it props in
+         List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets)
+      l
+
+  let create_proof_task_box l ~qed ~block_start:lemma =
+    if not (topo_invariant l) then anomaly (str "overlapping boxes");
+    vcs := create_property !vcs l (ProofTask { qed; lemma })
+  let create_proof_block ({ block_start; block_stop} as decl) name =
+    let l = nodes_in_slice ~block_start ~block_stop in
+    if not (topo_invariant l) then anomaly (str "overlapping boxes");
+    vcs := create_property !vcs l (ProofBlock (decl, name))
+  let box_of id = List.map Dag.Property.data (property_of !vcs id)
+  let delete_boxes_of id =
+    List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id)
+  let proof_task_box_of id =
+    match
+      CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id)
+    with
+    | [] -> None
+    | [x] -> Some x
+    | _ -> anomaly (str "node with more than 1 proof task box")
 
   let gc () =
     let old_vcs = !vcs in
     let new_vcs, erased_nodes = gc old_vcs in
-    Vcs_.NodeSet.iter (fun id ->
+    Stateid.Set.iter (fun id ->
         match (Vcs_aux.visit old_vcs id).step with
         | `Qed ({ fproof = Some (_, cancel_switch) }, _)
-        | `Cmd { cqueue = `TacQueue cancel_switch }
+        | `Cmd { cqueue = `TacQueue (_,_,cancel_switch) }
         | `Cmd { cqueue = `QueryQueue cancel_switch } ->
              cancel_switch := true
         | _ -> ())
@@ -583,7 +720,10 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 let state_of_id id =
-  try `Valid (VCS.get_info id).state
+  try match (VCS.get_info id).state with
+    | Valid s -> `Valid (Some s)
+    | Error (e,_) -> `Error e
+    | Empty -> `Valid None
   with VCS.Expired -> `Expired
 
 
@@ -603,9 +743,10 @@ module State : sig
 
   val install_cached : Stateid.t -> unit
   val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
+  val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
 
 
-  val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn
+  val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn
   (* to send states across worker/master *)
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
@@ -634,10 +775,9 @@ end = struct (* {{{ *)
     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)
+    (fun () -> Obj.magic (freeze_global_state `No, !cur_id))
+    (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i)
   
   type frozen_state = state
   type proof_part =
@@ -649,51 +789,60 @@ end = struct (* {{{ *)
     proof,
     Summary.project_summary (States.summary_of_state system) summary_pstate
 
-  let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
+  let freeze marshallable id =
+    VCS.set_state id (Valid (freeze_global_state marshallable))
+  let freeze_invalid id iexn = VCS.set_state id (Error iexn)
 
-  let is_cached ?(cache=`No) id =
+  let is_cached ?(cache=`No) id only_valid =
     if Stateid.equal id !cur_id then
       try match VCS.get_info id with
-        | { state = None } when cache = `Yes -> freeze `No id; true
-        | { state = None } when cache = `Shallow -> freeze `Shallow id; true
+        | { state = Empty } when cache = `Yes -> freeze `No id; true
+        | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true
         | _ -> true
       with VCS.Expired -> false
     else
       try match VCS.get_info id with
-        | { state = Some _ } -> true
-        | _ -> false 
+        | { state = Empty } -> false
+        | { state = Valid _ } -> true
+        | { state = Error _ } -> not only_valid
       with VCS.Expired -> false
 
+  let is_cached_and_valid ?cache id = is_cached ?cache id true
+  let is_cached ?cache id = is_cached ?cache id 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
+    match VCS.get_info id with
+    | { state = Valid s } ->
+         if Stateid.equal id !cur_id then () (* optimization *)
+         else begin unfreeze_global_state s; cur_id := id end
+    | { state = Error ie } -> cur_id := id; Exninfo.iraise ie 
+    | _ ->
+        (* coqc has a 1 slot cache and only for valid states *)
+        if interactive () = `No && Stateid.equal id !cur_id then ()
+        else anomaly (str "installing a non cached state")
 
   let get_cached id =
     try match VCS.get_info id with
-    | { state = Some s } -> s
+    | { state = Valid s } -> s
     | _ -> anomaly (str "not a cached state")
     with VCS.Expired -> anomaly (str "not a cached state (expired)")
 
   let assign id what =
-    if VCS.get_state id <> None then () else
+    if VCS.get_state id <> Empty then () else
     try match what with
     | `Full s ->
          let s =
            try
             let prev = (VCS.visit id).next in
-            if is_cached prev
+            if is_cached_and_valid prev
             then { s with proof = 
               Proof_global.copy_terminators
                 ~src:(get_cached prev).proof ~tgt:s.proof }
             else s
            with VCS.Expired -> s in
-         VCS.set_state id s
+         VCS.set_state id (Valid s)
     | `Proof(ontop,(pstate,counters)) ->
-         if is_cached ontop then
+         if is_cached_and_valid ontop then
            let s = get_cached ontop in
            let s = { s with proof =
              Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
@@ -702,17 +851,17 @@ end = struct (* {{{ *)
                (Summary.surgery_summary
                  (States.summary_of_state s.system)
                counters) } in
-           VCS.set_state id s
+           VCS.set_state id (Valid s)
     with VCS.Expired -> ()
 
-  let exn_on id ?valid (e, info) =
+  let exn_on id ~valid (e, info) =
     match Stateid.get info with
     | Some _ -> (e, info)
     | None ->
         let loc = Option.default Loc.ghost (Loc.get_loc info) in
         let (e, info) = Hooks.(call_process_error_once (e, info)) in
         Hooks.(call execution_error id loc (iprint (e, info)));
-        (e, Stateid.add info ?valid id)
+        (e, Stateid.add info ~valid id)
 
   let same_env { system = s1 } { system = s2 } =
     let s1 = States.summary_of_state s1 in
@@ -724,12 +873,12 @@ end = struct (* {{{ *)
   let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
   =
-    feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
+    feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
     let str_id = Stateid.to_string id in
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
     try
-      prerr_endline("defining "^str_id^" (cache="^
+      prerr_endline (fun () -> "defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
@@ -737,24 +886,27 @@ end = struct (* {{{ *)
       fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
-      prerr_endline ("setting cur id to "^str_id);
+      prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
         Hooks.(call state_computed id ~in_cache:false);
-      VCS.reached id true;
+      VCS.reached id;
       if Proof_global.there_are_pending_proofs () then
         VCS.goals id (Proof_global.get_open_goals ())
     with e ->
-      let (e, info) = Errors.push e in
+      let (e, info) = CErrors.push e in
       let good_id = !cur_id in
       cur_id := Stateid.dummy;
-      VCS.reached id false;
-      Hooks.(call unreachable_state id (e, info));
-      match Stateid.get info, safe_id with
-      | None, None -> iraise (exn_on id ~valid:good_id (e, info))
-      | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
-      | Some _, None -> iraise (e, info)
-      | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at)
+      VCS.reached id;
+      let ie =
+        match Stateid.get info, safe_id with
+        | None, None -> (exn_on id ~valid:good_id (e, info))
+        | None, Some good_id -> (exn_on id ~valid:good_id (e, info))
+        | Some _, None -> (e, info)
+        | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
+      if cache = `Yes || cache = `Shallow then freeze_invalid id ie;
+      Hooks.(call unreachable_state id ie);
+      Exninfo.iraise ie
 
 end (* }}} *)
 
@@ -830,7 +982,7 @@ end = struct (* {{{ *)
   let back_safe () =
     let id =
       fold_until (fun n (id,_,_,_,_) ->
-        if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
+        if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n))
         0 (VCS.get_branch_pos (VCS.current_branch ())) in
     backto id
 
@@ -840,8 +992,6 @@ end = struct (* {{{ *)
       | 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 =
@@ -891,8 +1041,8 @@ end = struct (* {{{ *)
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
-       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
-       VtStm (VtBack Stateid.initial, true), VtNow
+       CErrors.errorlabstrm "undo_vernac_classifier"
+        (str "Cannot undo")
 
 end (* }}} *)
 
@@ -925,10 +1075,78 @@ let record_pb_time proof_name loc time =
   end
  
 exception RemoteException of std_ppcmds
-let _ = Errors.register_handler (function
+let _ = CErrors.register_handler (function
   | RemoteException ppcmd -> ppcmd
   | _ -> raise Unhandled)
 
+(****************** proof structure for error recovery ************************)
+(******************************************************************************)
+
+type document_node = {
+  indentation : int;
+  ast : Vernacexpr.vernac_expr;
+  id : Stateid.t;
+}
+
+type document_view = {
+  entry_point : document_node;
+  prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+  document_view -> static_block_declaration option
+
+type recovery_action = {
+  base_state : Stateid.t;
+  goals_to_admit : Goal.goal list;
+  recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+let proof_block_delimiters = ref []
+
+let register_proof_block_delimiter name static dynamic =
+  if List.mem_assoc name !proof_block_delimiters then
+    CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+  proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
+
+let mk_doc_node id = function
+  | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
+       Some { indentation; ast = expr; id }
+  | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } ->
+       Some { indentation; ast = expr; id }
+  | _ -> None
+let prev_node { id } =
+  let id = (VCS.visit id).next in
+  mk_doc_node id (VCS.visit id)
+let cur_node id = mk_doc_node id (VCS.visit id)
+
+let is_block_name_enabled name =
+  match !Flags.async_proofs_tac_error_resilience with
+  | `None -> false
+  | `All -> true
+  | `Only l -> List.mem name l
+
+let detect_proof_block id name =
+  let name = match name with None -> "indent" | Some x -> x in   
+  if is_block_name_enabled name &&
+     (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ())
+  then (
+  match cur_node id with
+  | None -> ()
+  | Some entry_point -> try
+      let static, _ = List.assoc name !proof_block_delimiters in
+      begin match static { prev_node; entry_point } with
+      | None -> ()
+      | Some ({ block_start; block_stop } as decl) ->
+          VCS.create_proof_block decl name
+      end
+    with Not_found ->
+      CErrors.errorlabstrm "STM"
+        (str "Unknown proof block delimiter " ++ str name)
+  )
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
 
@@ -1034,7 +1252,7 @@ end = struct (* {{{ *)
         try Some (ReqBuildProof ({
           Stateid.exn_info = t_exn_info;
           stop = t_stop;
-          document = VCS.slice ~start:t_start ~stop:t_stop;
+          document = VCS.slice ~block_start:t_start ~block_stop:t_stop;
           loc = t_loc;
           uuid = t_uuid;
           name = t_name }, t_drop, t_states))
@@ -1046,7 +1264,7 @@ end = struct (* {{{ *)
         List.iter (fun (id,s) -> State.assign id s) l; `End
     | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
               RespBuiltProof (pl, time) ->
-        feedback (Feedback.InProgress ~-1);
+        feedback (InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time t_name t_loc time;
         if !Flags.async_proofs_full || t_drop
@@ -1054,7 +1272,7 @@ end = struct (* {{{ *)
         else `End
     | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
-        feedback (Feedback.InProgress ~-1);
+        feedback (InProgress ~-1);
         let info = Stateid.add ~valid Exninfo.null e_error_at in
         let e = (RemoteException e_msg, info) in
         t_assign (`Exn e);
@@ -1070,7 +1288,7 @@ end = struct (* {{{ *)
         let e = (RemoteException (strbrk s), info) in
         t_assign (`Exn e);
         Hooks.(call execution_error start Loc.ghost (strbrk s));
-        feedback (Feedback.InProgress ~-1)
+        feedback (InProgress ~-1)
 
   let build_proof_here ~drop_pt (id,valid) loc eop =
     Future.create (State.exn_on id ~valid) (fun () ->
@@ -1081,7 +1299,7 @@ end = struct (* {{{ *)
       Aux_file.record_in_aux_at loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       let p = Proof_global.return_proof ~allow_partial:drop_pt () in
-      if drop_pt then Pp.feedback ~state_id:id Feedback.Complete;
+      if drop_pt then feedback ~id:(State id) Complete;
       p)
 
   let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1105,30 +1323,31 @@ end = struct (* {{{ *)
             Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
           vernac_interp stop
             ~proof:(pobject, terminator)
-            { verbose = false; loc;
+            { verbose = false; loc; indentation = 0; strlen = 0;
               expr = (VernacEndProof (Proved (Opaque None,None))) }) in
         ignore(Future.join checked_proof);
       end;
       RespBuiltProof(proof,time)
     with
-    | e when Errors.noncritical e || e = Stack_overflow ->
-        let (e, info) = Errors.push e in
+    | e when CErrors.noncritical e || e = Stack_overflow ->
+        let (e, info) = CErrors.push e in
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
         let e_error_at, e_safe_id = match Stateid.get info with
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        prerr_endline "failed with the following exception:";
-        prerr_endline (string_of_ppcmds e_msg);
-        let e_safe_states = List.filter State.is_cached my_states in
+        prerr_endline (fun () -> "failed with the following exception:");
+        prerr_endline (fun () -> string_of_ppcmds e_msg);
+        let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
   
   let perform_states query =
     if query = [] then [] else
-    let is_tac = function
-      | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
-      | _ -> false in
+    let is_tac e = match classify_vernac e with
+    | VtProofStep _, _ -> true
+    | _ -> false
+    in
     let initial = 
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
@@ -1138,19 +1357,19 @@ end = struct (* {{{ *)
       let prev =
         try
           let { next = prev; step } = VCS.visit id in
-          if State.is_cached prev && List.mem prev seen
+          if State.is_cached_and_valid prev && List.mem prev seen
           then Some (prev, State.get_cached prev, step)
           else None
         with VCS.Expired -> None in
       let this = 
-        if State.is_cached id then Some (State.get_cached id) else None in
+        if State.is_cached_and_valid id then Some (State.get_cached id) else None in
       match prev, this with
       | _, None -> None
       | Some (prev, o, `Cmd { cast = { expr }}), Some n
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_warning (str "STM: sending back a fat state");
+          msg_debug (str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
@@ -1173,7 +1392,7 @@ end = struct (* {{{ *)
         "The system state could not be sent to the worker process. "^
         "Falling back to local, lazy, evaluation."));
       t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
-      feedback (Feedback.InProgress ~-1)
+      feedback (InProgress ~-1)
 
 end (* }}} *)
 
@@ -1183,7 +1402,7 @@ and Slaves : sig
   (* (eventually) remote calls *)
   val build_proof :
     loc:Loc.t -> drop_pt:bool ->
-    exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
+    exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t ->
       name:string -> future_proof * cancel_switch
 
   (* blocking function that waits for the task queue to be empty *)
@@ -1221,8 +1440,8 @@ end = struct (* {{{ *)
 
   let check_task_aux extra name l i =
     let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
-    msg_info(
-      str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+    Flags.if_verbose msg_info
+      (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
     VCS.restore document;
     let start =
       let rec aux cur =
@@ -1245,15 +1464,15 @@ end = struct (* {{{ *)
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~cache:`No start;
       vernac_interp stop ~proof
-        { verbose = false; loc;
+        { verbose = false; loc; indentation = 0; strlen = 0;
           expr = (VernacEndProof (Proved (Opaque None,None))) };
       `OK proof
       end
     with e ->
-      let (e, info) = Errors.push e in
+      let (e, info) = CErrors.push e in
       (try match Stateid.get info with
       | None ->
-          pperrnl (
+          msg_error (
             str"File " ++ str name ++ str ": proof of " ++ str r_name ++
             spc () ++ iprint (e, info))
       | Some (_, cur) ->
@@ -1263,12 +1482,12 @@ end = struct (* {{{ *)
           | { step = `Qed ( { qast = { loc } }, _) } 
           | { step = `Sideff (`Ast ( { loc }, _)) } ->
               let start, stop = Loc.unloc loc in
-              pperrnl (
+              msg_error (
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
                 str ": chars " ++ int start ++ str "-" ++ int stop ++
                 spc () ++ iprint (e, info))
           | _ ->
-              pperrnl (
+              msg_error (
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
                 spc () ++ iprint (e, info))
     with e ->
@@ -1328,7 +1547,6 @@ end = struct (* {{{ *)
   let set_perspective idl =
     ProofTask.set_perspective idl;
     TaskQueue.broadcast (Option.get !queue);
-    let open Stateid in
     let open ProofTask in
     let overlap s1 s2 =
       List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in
@@ -1343,7 +1561,7 @@ end = struct (* {{{ *)
        BuildProof { t_states = s2 } -> overlap_rel s1 s2
      | _ -> 0)
 
-  let build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name:pname =
+  let build_proof ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname =
     let id, valid as t_exn_info = exn_info in
     let cancel_switch = ref false in
     if TaskQueue.n_workers (Option.get !queue) = 0 then
@@ -1352,21 +1570,21 @@ end = struct (* {{{ *)
          Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
         let task = ProofTask.(BuildProof {
-          t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt;
+          t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt;
           t_assign = assign; t_loc = loc; t_uuid; t_name = pname;
-          t_states = VCS.nodes_in_slice ~start ~stop }) in
+          t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in
         TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
         f, cancel_switch
       end else
-        ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch
+        ProofTask.build_proof_here ~drop_pt t_exn_info loc block_stop, cancel_switch
     else 
       let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
-      feedback (Feedback.InProgress 1);
+      feedback (InProgress 1);
       let task = ProofTask.(BuildProof {
-        t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt;
+        t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt;
         t_loc = loc; t_uuid; t_name = pname;
-        t_states = VCS.nodes_in_slice ~start ~stop }) in
+        t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in
       TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
       f, cancel_switch
 
@@ -1385,7 +1603,7 @@ end = struct (* {{{ *)
              | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
-    prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
     reqs
 
   let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1399,10 +1617,11 @@ and TacTask : sig
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : ast;
+    t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
+  exception NoProgress
 
   include AsyncTaskQueue.Task with type task := task
 
@@ -1416,7 +1635,7 @@ end = struct (* {{{ *)
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : ast;
+    t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1425,13 +1644,15 @@ end = struct (* {{{ *)
     r_state    : Stateid.t;
     r_state_fb : Stateid.t;
     r_document : VCS.vcs option;
-    r_ast      : ast;
+    r_ast      : int * aast;
     r_goal     : Goal.goal;
     r_name     : string }
 
   type response =
     | RespBuiltSubProof of output
     | RespError of std_ppcmds
+    | RespNoProgress
+  exception NoProgress
 
   let name = ref "tacworker"
   let extra_env () = [||]
@@ -1445,7 +1666,7 @@ end = struct (* {{{ *)
       r_state_fb = t_state_fb;
       r_document =
         if age <> `Fresh then None
-        else Some (VCS.slice ~start:t_state ~stop:t_state);
+        else Some (VCS.slice ~block_start:t_state ~block_stop:t_state);
       r_ast      = t_ast;
       r_goal     = t_goal;
       r_name     = t_name }
@@ -1454,9 +1675,13 @@ end = struct (* {{{ *)
   let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
     match resp with
     | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+    | RespNoProgress ->
+        let e = (NoProgress, Exninfo.null) in
+        t_assign (`Exn e);
+        t_kill ();
+        `Stay ((),[])
     | RespError msg ->
-        let info = Stateid.add ~valid:t_state Exninfo.null t_state_fb in
-        let e = (RemoteException msg, info) in
+        let e = (RemoteException msg, Exninfo.null) in
         t_assign (`Exn e);
         t_kill ();
         `Stay ((),[])
@@ -1469,36 +1694,37 @@ end = struct (* {{{ *)
     | Some { t_kill } -> t_kill ()
     | _ -> ()
  
+  let command_focus = Proof.new_focus_kind ()
+  let focus_cond = Proof.no_cond command_focus
+
   let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
     Option.iter VCS.restore vcs;
     try
       Reach.known_state ~cache:`No id;
-      let t, uc = Future.purify (fun () ->
+      Future.purify (fun () ->
        let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
        if not (
          Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
-         List.for_all (fun (_,bo,ty) ->
-            Evarutil.is_ground_term sigma0 ty &&
-            Option.cata (Evarutil.is_ground_term sigma0) true bo)
-           Evd.(evar_context g))
+         List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+                      Evd.(evar_context g))
        then
-         Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
+         CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
-        vernac_interp r_state_fb r_ast;
+        let (i, ast) = r_ast in
+        Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+        vernac_interp r_state_fb ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
-        | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
+        | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
-              t, Evd.evar_universe_context sigma
-            else Errors.errorlabstrm "Stm" (str"The solution is not ground")
+              RespBuiltSubProof (t, Evd.evar_universe_context sigma)
+            else CErrors.errorlabstrm "STM" (str"The solution is not ground")
        end) ()
-     in
-       RespBuiltSubProof (t,uc)
-    with e when Errors.noncritical e -> RespError (Errors.print e)
+    with e when CErrors.noncritical e -> RespError (CErrors.print e)
 
   let name_of_task { t_name } = t_name
   let name_of_request { r_name } = r_name
@@ -1508,19 +1734,22 @@ end (* }}} *)
 and Partac : sig
 
   val vernac_interp :
-    cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit
+    solve:bool -> abstract:bool -> cancel_switch ->
+    int -> Stateid.t -> Stateid.t -> aast ->
+      unit
 
 end = struct (* {{{ *)
     
   module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
 
-  let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
-    let e, etac, time, fail =
+  let vernac_interp ~solve ~abstract cancel nworkers safe_id id
+    { indentation; verbose; loc; expr = e; strlen }
+  =
+    let e, time, fail =
       let rec find time fail = function
-        | VernacSolve(_,_,re,b) -> re, b, time, fail
-        | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
+        | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
         | VernacFail e -> find time true e
-        | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
+        | _ -> e, time, fail in find false false e in
     Hooks.call Hooks.with_fail fail (fun () ->
     (if time then System.with_time false else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -1532,51 +1761,58 @@ end = struct (* {{{ *)
           Future.create_delegate
             ~name:(Printf.sprintf "subgoal %d" i)
             (State.exn_on id ~valid:safe_id) in
-        let t_ast =
-          { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
+        let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task queue
           ({ t_state = safe_id; t_state_fb = id;
             t_assign = assign; t_ast; t_goal = g; t_name;
-            t_kill = (fun () -> TaskQueue.cancel_all queue) }, cancel);
-        Goal.uid g,f)
+            t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) },
+           cancel);
+        g,f)
         1 goals in
       TaskQueue.join queue;
       let assign_tac : unit Proofview.tactic =
-        Proofview.V82.tactic (fun gl ->
-          let open Tacmach in
-          let sigma, g = project gl, sig_it gl in
-          let gid = Goal.uid g in
-          let f =
-            try List.assoc gid res
-            with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
-          if Future.is_over f then
+        Proofview.(Goal.nf_enter { Goal.enter = fun g ->
+        let gid = Goal.goal g in
+        let f =
+          try List.assoc gid res
+          with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in
+        if not (Future.is_over f) then
+          (* One has failed and cancelled the others, but not this one *)
+          if solve then Tacticals.New.tclZEROMSG
+            (str"Interrupted by the failure of another goal")
+          else tclUNIT ()
+        else
+          let open Notations in
+          try
             let pt, uc = Future.join f in
-            prerr_endline (string_of_ppcmds(hov 0 (
-              str"g=" ++ str gid ++ spc () ++
+            prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+              str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
               str"uc=" ++ Evd.pr_evar_universe_context uc)));
-            let sigma = Goal.V82.partial_solution sigma g pt in
-            let sigma = Evd.merge_universe_context sigma uc in
-            re_sig [] sigma
-          else (* One has failed and cancelled the others, but not this one *)
-            re_sig [g] sigma) in
+            (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
+              (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
+              Tactics.exact_no_check pt)
+          with TacTask.NoProgress ->
+            if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
+        })
+      in
       Proof.run_tactic (Global.env()) assign_tac p)))) ())
   
 end (* }}} *)
 
 and QueryTask : sig
 
-  type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+  type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
   include AsyncTaskQueue.Task with type task := task
 
 end = struct (* {{{ *)
   
   type task =
-    { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+    { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
   
   type request =
-    { r_where : Stateid.t ; r_for : Stateid.t ; r_what : ast; r_doc : VCS.vcs }
+    { r_where : Stateid.t ; r_for : Stateid.t ; r_what : aast; r_doc : VCS.vcs }
   type response = unit
 
   let name = ref "queryworker"
@@ -1588,7 +1824,7 @@ end = struct (* {{{ *)
     try Some {
       r_where = t_where;
       r_for   = t_for;
-      r_doc   = VCS.slice ~start:t_where ~stop:t_where;
+      r_doc   = VCS.slice ~block_start:t_where ~block_stop:t_where;
       r_what  = t_what }
     with VCS.Expired -> None
   
@@ -1608,11 +1844,11 @@ end = struct (* {{{ *)
     Reach.known_state ~cache:`No r_where;
     try
       vernac_interp r_for { r_what with verbose = true };
-      feedback ~state_id:r_for Feedback.Processed     
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in
-      let msg = string_of_ppcmds (iprint e) in
-      feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
+      feedback ~id:(State r_for) Processed
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      let msg = pp_to_richpp (iprint e) in
+      feedback ~id:(State r_for) (Message (Error, None, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -1622,7 +1858,7 @@ end (* }}} *)
 and Query : sig 
 
   val init : unit -> unit
-  val vernac_interp : cancel_switch -> Stateid.t ->  Stateid.t -> ast -> unit
+  val vernac_interp : cancel_switch -> Stateid.t ->  Stateid.t -> aast -> unit
 
 end = struct (* {{{ *)
 
@@ -1633,7 +1869,7 @@ end = struct (* {{{ *)
   let vernac_interp switch prev id q =
     assert(TaskQueue.n_workers (Option.get !queue) > 0);
     TaskQueue.enqueue_task (Option.get !queue)
-      QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch)
+      QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch)
 
   let init () = queue := Some (TaskQueue.create
     (if !Flags.async_proofs_full then 1 else 0))
@@ -1659,12 +1895,18 @@ let async_policy () =
     (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
 
 let delegate name =
-  let time = get_hint_bp_time name in
-  time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
-              || !Flags.async_proofs_full
+     get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
+  || !Flags.compilation_mode = Flags.BuildVio
+  || !Flags.async_proofs_full
+ 
+let warn_deprecated_nested_proofs =
+  CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
+         (fun () ->
+          strbrk ("Nested proofs are deprecated and will "^
+                    "stop working in a future Coq version"))
 
 let collect_proof keep cur hd brkind id =
- prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
  let name = function
    | [] -> no_name
@@ -1684,16 +1926,20 @@ let collect_proof keep cur hd brkind id =
  let has_proof_no_using = function
    | Some (_, { expr = VernacProof(_,None) }) -> true
    | _ -> false in
- let may_pierce_opaque = function
-   | { expr = VernacPrint (PrintName _) } -> true
-   | _ -> false in
+ let too_complex_to_delegate = function
+   | { expr = (VernacDeclareModule _
+              | VernacDefineModule _
+              | VernacDeclareModuleType _
+              | VernacInclude _) } -> true
+   | { expr =  (VernacRequire _ | VernacImport _) } -> true
+   | ast -> may_pierce_opaque ast in
  let parent = function Some (p, _) -> p | None -> assert false in
  let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
     | (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
-      when may_pierce_opaque x -> `Sync(no_name,None,`Print)
+      when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
     | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
@@ -1707,7 +1953,7 @@ let collect_proof keep cur hd brkind id =
         let name = name ids in
         `ASync (parent last,proof_using_ast last,accn,name,delegate name)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
-       has_proof_no_using last && not (State.is_cached (parent last)) &&
+       has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
        !Flags.compilation_mode = Flags.BuildVio ->
         assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
         (try
@@ -1723,8 +1969,7 @@ let collect_proof keep cur hd brkind id =
         let name = name ids in
         `MaybeASync (parent last, None, accn, name, delegate name)
     | `Sideff _ ->
-        Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^
-           "stop working in the next Coq version")));
+       warn_deprecated_nested_proofs ();
         `Sync (no_name,None,`NestedProof)
     | _ -> `Sync (no_name,None,`Unknown) in
  let make_sync why = function
@@ -1743,7 +1988,7 @@ let collect_proof keep cur hd brkind id =
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
        else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
-          (not(State.is_cached id) || !Flags.async_proofs_full)
+          (not(State.is_cached_and_valid id) || !Flags.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
@@ -1761,7 +2006,7 @@ let string_of_reason = function
   | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
   | `Unknown -> "unsupported case"
 
-let log_string s = prerr_debug ("STM: " ^ s)
+let log_string s = prerr_debug (fun () -> "STM: " ^ s)
 let log_processing_async id name = log_string Printf.(sprintf
   "%s: proof %s: asynch" (Stateid.to_string id) name
 )
@@ -1773,6 +2018,71 @@ let log_processing_sync id name reason = log_string Printf.(sprintf
 let wall_clock_last_fork = ref 0.0
 
 let known_state ?(redefine_qed=false) ~cache id =
+ 
+  let error_absorbing_tactic id blockname exn =
+    (* We keep the static/dynamic part of block detection separate, since
+       the static part could be performed earlier.  As of today there is
+       no advantage in doing so since no UI can exploit such piece of info *)
+    detect_proof_block id blockname;
+
+    let boxes = VCS.box_of id in
+    let valid_boxes = CList.map_filter (function
+      | ProofBlock ({ block_stop } as decl, name) when Stateid.equal block_stop id ->
+          Some (decl, name)
+      | _ -> None) boxes in
+    assert(List.length valid_boxes < 2);
+    if valid_boxes = [] then iraise exn
+    else
+      let decl, name = List.hd valid_boxes in
+      try
+        let _, dynamic_check = List.assoc name !proof_block_delimiters in
+        match dynamic_check decl with
+        | `Leaks -> iraise exn
+        | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
+           let tac =
+             let open Proofview.Notations in
+             Proofview.Goal.nf_enter { enter = fun gl ->
+               if CList.mem_f Evar.equal
+                 (Proofview.Goal.goal gl) goals_to_admit then
+             Proofview.give_up else Proofview.tclUNIT ()
+               } in
+           match (VCS.get_info base_state).state with
+           | Valid { proof } ->
+               Proof_global.unfreeze proof;
+               Proof_global.with_current_proof (fun _ p ->
+                 feedback ~id:(State id) Feedback.AddedAxiom;
+                 fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+               Option.iter (fun expr -> vernac_interp id {
+                  verbose = true; loc = Loc.ghost; expr; indentation = 0;
+                  strlen = 0 })
+               recovery_command
+           | _ -> assert false
+        end
+      with Not_found ->
+          CErrors.errorlabstrm "STM"
+            (str "Unknown proof block delimiter " ++ str name)
+  in
+
+  (* Absorb tactic errors from f () *)
+  let resilient_tactic id blockname f =
+    if !Flags.async_proofs_tac_error_resilience = `None ||
+       (Flags.async_proofs_is_master () &&
+        !Flags.async_proofs_mode = Flags.APoff)
+    then f ()
+    else
+      try f ()
+      with e when CErrors.noncritical e ->
+        let ie = CErrors.push e in
+        error_absorbing_tactic id blockname ie in
+  (* Absorb errors from f x *)
+  let resilient_command f x =
+    if not !Flags.async_proofs_cmd_error_resilience ||
+       (Flags.async_proofs_is_master () &&
+        !Flags.async_proofs_mode = Flags.APoff)
+    then f x
+    else
+      try f x
+      with e when CErrors.noncritical e -> () in
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
@@ -1782,18 +2092,18 @@ let known_state ?(redefine_qed=false) ~cache id =
   let inject_non_pstate (s,l) =
     Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
   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;
+  let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
+    prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+    reach ~safe_id id;
     cherry_pick_non_pstate ()) id
 
   (* traverses the dag backward from nodes being already calculated *)
-  and reach ?(redefine_qed=false) ?(cache=cache) id =
-    prerr_endline ("reaching: " ^ Stateid.to_string id);
+  and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
+    prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
-      State.install_cached id;
       Hooks.(call state_computed id ~in_cache:true);
-      prerr_endline ("reached (cache)")
+      prerr_endline (fun () -> "reached (cache)");
+      State.install_cached id
     end else
     let step, cache_step, feedback_processed =
       let view = VCS.visit id in
@@ -1801,46 +2111,58 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Alias (id,_) -> (fun () ->
             reach view.next; reach id
           ), cache, true
-      | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
-            reach ~cache:`Shallow view.next;
-            Hooks.(call tactic_being_run true); 
-            Partac.vernac_interp
-              cancel !Flags.async_proofs_n_tacworkers view.next id x;
-            Hooks.(call tactic_being_run false)
+      | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
+            reach view.next), cache, true
+      | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel); cblock } ->
+          (fun () ->
+            resilient_tactic id cblock (fun () ->
+              reach ~cache:`Shallow view.next;
+              Hooks.(call tactic_being_run true); 
+              Partac.vernac_interp ~solve ~abstract
+                cancel !Flags.async_proofs_n_tacworkers view.next id x;
+              Hooks.(call tactic_being_run false))
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
             reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
-      | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
-            reach view.next;
-            if ctac then Hooks.(call tactic_being_run true); 
+      | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
+            resilient_tactic id cblock (fun () ->
+              reach view.next;
+              Hooks.(call tactic_being_run true); 
+              vernac_interp id x;
+              Hooks.(call tactic_being_run false)); 
+	    if eff then update_global_env ()
+          ), (if eff then `Yes else cache), true
+      | `Cmd { cast = x; ceff = eff } -> (fun () ->
+            resilient_command reach view.next;
             vernac_interp id x;
-            if ctac then Hooks.(call tactic_being_run false); 
-	    if eff then update_global_env ()), cache, true
+	    if eff then update_global_env ()
+          ), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
-            reach view.next; vernac_interp id x;
+            resilient_command reach view.next;
+            vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
-      | `Fork ((x,_,_,_), Some prev) -> (fun () ->
+      | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
             reach ~cache:`Shallow prev;
             reach view.next;
             (try vernac_interp id x;
-            with e when Errors.noncritical e ->
-              let (e, info) = Errors.push e in
+            with e when CErrors.noncritical e ->
+              let (e, info) = CErrors.push e in
               let info = Stateid.add info ~valid:prev id in
               iraise (e, info));
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
-          | `ASync (start, pua, nodes, name, delegate) -> (fun () ->
+          | `ASync (block_start, pua, nodes, name, delegate) -> (fun () ->
                 assert(keep == VtKeep || keep == VtKeepAsAxiom);
                 let drop_pt = keep == VtKeepAsAxiom in
-                let stop, exn_info, loc = eop, (id, eop), x.loc in
+                let block_stop, exn_info, loc = eop, (id, eop), x.loc in
                 log_processing_async id name;
-                VCS.create_cluster nodes ~qed:id ~start;
+                VCS.create_proof_task_box nodes ~qed:id ~block_start;
                 begin match brinfo, qed.fproof with
                 | { VCS.kind = `Edit _ }, None -> assert false
                 | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
@@ -1854,19 +2176,22 @@ let known_state ?(redefine_qed=false) ~cache id =
                         ^"the proof's statement to avoid that."));
                     let fp, cancel =
                       Slaves.build_proof
-                        ~loc ~drop_pt ~exn_info ~start ~stop ~name in
+                        ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
                     Future.replace ofp fp;
-                    qed.fproof <- Some (fp, cancel)
+                    qed.fproof <- Some (fp, cancel);
+                    (* We don't generate a new state, but we still need
+                     * to install the right one *)
+                    State.install_cached id
                 | { VCS.kind = `Proof _ }, Some _ -> assert false
                 | { VCS.kind = `Proof _ }, None ->
-                    reach ~cache:`Shallow start;
+                    reach ~cache:`Shallow block_start;
                     let fp, cancel =
                       if delegate then
                         Slaves.build_proof
-                          ~loc ~drop_pt ~exn_info ~start ~stop ~name
+                          ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
                       else
                         ProofTask.build_proof_here
-                          ~drop_pt exn_info loc stop, ref false
+                          ~drop_pt exn_info loc block_stop, ref false
                     in
                     qed.fproof <- Some (fp, cancel);
                     let proof =
@@ -1874,7 +2199,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     vernac_interp id ~proof x;
-                    feedback ~state_id:id Feedback.Incomplete
+                    feedback ~id:(State id) Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
                 Proof_global.discard_all ()
@@ -1921,15 +2246,15 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Sideff (`Id origin) -> (fun () ->
             reach view.next;
-            inject_non_pstate (pure_cherry_pick_non_pstate origin);
+            inject_non_pstate (pure_cherry_pick_non_pstate view.next origin);
           ), cache, true
     in
     let cache_step =
       if !Flags.async_proofs_cache = Some Flags.Force then `Yes
       else cache_step in
-    State.define
+    State.define ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    prerr_endline ("reached: "^ Stateid.to_string id) in
+    prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
 end (* }}} *)
@@ -1944,7 +2269,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline "Initializing workers";
+    prerr_endline (fun () -> "Initializing workers");
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
@@ -1963,7 +2288,7 @@ let observe id =
     Reach.known_state ~cache:(interactive ()) id;
     VCS.print ()
   with e ->
-    let e = Errors.push e in
+    let e = CErrors.push e in
     VCS.print ();
     VCS.restore vcs;
     iraise e
@@ -1996,9 +2321,9 @@ let rec join_admitted_proofs id =
 let join () =
   finish ();
   wait ();
-  prerr_endline "Joining the environment";
+  prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
-  prerr_endline "Joining Admitted proofs";
+  prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
   VCS.print ()
@@ -2011,28 +2336,26 @@ let check_task name (tasks,rcbackup) i =
   let vcs = VCS.backup () in
   try
     let rc = Future.purify (Slaves.check_task name tasks) i in
-    pperr_flush ();
     VCS.restore vcs;
     rc
-  with e when Errors.noncritical e -> VCS.restore vcs; false
+  with e when CErrors.noncritical e -> VCS.restore vcs; false
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
 let finish_tasks name u d p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
   let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
     let u = Future.purify (Slaves.finish_task name u d p t) i in
-    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
-    pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+    let e = CErrors.push e in
+    msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
-let merge_proof_branch ?valid ?id qast keep brname =
+let merge_proof_branch ~valid ?id qast keep brname =
   let brinfo = VCS.get_branch brname in
   let qed fproof = { qast; keep; brname; brinfo; fproof } in
   match brinfo with
@@ -2041,7 +2364,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
       let id = VCS.new_node ?id () in
       VCS.merge id ~ours:(Qed (qed None)) brname;
       VCS.delete_branch brname;
-      if keep <> VtDrop then VCS.propagate_sideff None;
+      VCS.propagate_sideff None;
       `Ok
   | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
       let ofp =
@@ -2055,12 +2378,12 @@ let merge_proof_branch ?valid ?id qast keep brname =
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
-       iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+       iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
 
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
 let handle_failure (e, info) vcs tty =
-  if e = Errors.Drop then iraise (e, info) else
+  if e = CErrors.Drop then iraise (e, info) else
   match Stateid.get info with
   | None ->
       VCS.restore vcs;
@@ -2072,9 +2395,9 @@ let handle_failure (e, info) vcs tty =
       end;
       VCS.print ();
       anomaly(str"error with no safe_id attached:" ++ spc() ++
-        Errors.iprint_no_report (e, info))
+        CErrors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
-      prerr_endline ("Failed at state " ^ Stateid.to_string id);
+      prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
       if tty && interactive () = `Yes then begin
         (* We stay on a valid state *)
@@ -2085,38 +2408,37 @@ let handle_failure (e, info) vcs tty =
       VCS.print ();
       iraise (e, info)
 
-let snapshot_vio ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_vo =
   finish ();
   if List.length (VCS.branches ()) > 1 then
-    Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+    CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())
 
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~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; loc; expr } in
-  prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
+let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+  ({ verbose; loc; expr } as x) c =
+  prerr_endline (fun () -> "{{{ 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);
+      prerr_endline (fun () ->
+        "  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 (VtJoinDocument, b), VtNow -> join (); `Ok
+      | VtStm (VtFinish, b),       VtNow -> finish (); `Ok
+      | VtStm (VtWait, b),     VtNow -> 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
+          VCS.print ~now:true (); `Ok
+      | VtStm (VtObserve id, b),   VtNow -> observe id; `Ok
       | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
                 |VtPrintDag |VtWait),_), VtLater ->
           anomaly(str"classifier: join actions cannot be classified as VtLater")
@@ -2125,9 +2447,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtStm (VtBack oid, true), w ->
           let id = VCS.new_node ~id:newtip () in
           let { mine; others } = Backtrack.branches_of oid in
+          let valid = VCS.get_branch_pos head in
           List.iter (fun branch ->
             if not (List.mem_assoc branch (mine::others)) then
-              ignore(merge_proof_branch x VtDrop branch))
+              ignore(merge_proof_branch ~valid x VtDrop branch))
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           let head = VCS.current_branch () in
@@ -2141,7 +2464,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
-          prerr_endline ("undo to state " ^ Stateid.to_string id);
+          prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2152,22 +2475,26 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtQuery (false,(report_id,route)), VtNow when tty = true ->
           finish ();
           (try Future.purify (vernac_interp report_id ~route)
-                  { verbose = true; loc; expr }
-           with e when Errors.noncritical e ->
-             let e = Errors.push e in
-             iraise (State.exn_on report_id e)); `Ok
+            {x with verbose = true }
+           with e when CErrors.noncritical e ->
+             let e = CErrors.push e in
+             iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
       | VtQuery (false,(report_id,route)), VtNow ->
           (try vernac_interp report_id ~route x
            with e ->
-             let e = Errors.push e in
-             iraise (State.exn_on report_id e)); `Ok
+             let e = CErrors.push e in
+             iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
       | VtQuery (true,(report_id,_)), w ->
           assert(Stateid.equal report_id Stateid.dummy);
           let id = VCS.new_node ~id:newtip () in
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
+            else if Flags.(!compilation_mode = BuildVio) &&
+                    VCS.((get_branch head).kind = `Master) &&
+                    may_pierce_opaque x
+                 then `SkipQueue 
             else `MainQueue in
-          VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
+          VCS.commit id (mkTransCmd x [] false queue);
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQuery (false,_), VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2190,7 +2517,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"VtProofMode must be executed VtNow")
       | VtProofMode mode, VtNow ->
           let id = VCS.new_node ~id:newtip () in
-          VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
+          VCS.commit id (mkTransCmd x [] false `MainQueue);
           List.iter
             (fun bn -> match VCS.get_branch bn with
             | { VCS.root; kind = `Master; pos } -> ()
@@ -2205,14 +2532,21 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           Backtrack.record ();
           finish ();
           `Ok
-      | VtProofStep paral, w ->
+      | VtProofStep { parallel; proof_block_detection = cblock }, w ->
           let id = VCS.new_node ~id:newtip () in
-          let queue = if paral then `TacQueue (ref false) else `MainQueue in
-          VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
+          let queue =
+            match parallel with
+            | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false)
+            | `No -> `MainQueue in
+          VCS.commit id (mkTransTac x cblock queue);
+          (* Static proof block detection delayed until an error really occurs.
+             If/when and UI will make something useful with this piece of info,
+             detection should occur here.
+          detect_proof_block id cblock; *)
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
-          let valid = if tty then Some(VCS.get_branch_pos head) else None in
-          let rc = merge_proof_branch ?valid ~id:newtip x keep head in
+          let valid = VCS.get_branch_pos head in
+          let rc = merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish ();
           rc
@@ -2222,15 +2556,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           vernac_interp (VCS.get_branch_pos head) x; `Ok
 
       | VtSideff l, w ->
+          let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
-          VCS.propagate_sideff (Some x);
+          VCS.commit id (mkTransCmd x l in_proof `MainQueue);
+          (* We can't replay a Definition since universes may be differently
+           * inferred.  This holds in Coq >= 8.5 *)
+	  let replay = match x.expr with
+	    | VernacDefinition(_, _, DefineBody _) -> None
+	    | _ -> Some x in
+	  VCS.propagate_sideff ~replay;
           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 in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
           let head_id = VCS.get_branch_pos head in
           Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
@@ -2240,17 +2581,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
             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
+            if not in_proof && 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";
+              let opacity_of_produced_term =
+                match x.expr with
+                (* This AST is ambiguous, hence we check it dynamically *)
+                | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+                | _ -> Doesn'tGuaranteeOpacity in
+              VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
+              let proof_mode = default_proof_mode () in
+              VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
+              Proof_global.activate_proof_mode proof_mode;
             end else begin
-	      VCS.commit id (Cmd {ctac = false; ceff = true;
-				    cast = x; cids = []; cqueue = `MainQueue});
-              VCS.propagate_sideff (Some x);
+              VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+              (* We hope it can be replayed, but we can't really know *)
+              VCS.propagate_sideff ~replay:(Some x);
               VCS.checkout_shallowest_proof_branch ();
             end in
           State.define ~safe_id:head_id ~cache:`Yes step id;
@@ -2260,49 +2606,56 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"classifier: VtUnknown must imply VtNow")
     end in
     (* Proof General *)
-    begin match v with 
+    begin match expr with 
       | VernacStm (PGLast _) ->
         if not (VCS.Branch.equal head VCS.Branch.master) then
           vernac_interp Stateid.dummy
-            { verbose = true; loc = Loc.ghost;
+            { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
               expr = VernacShow (ShowGoal OpenSubgoals) }
       | _ -> ()
     end;
-    prerr_endline "processed }}}";
+    prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
   with e ->
-    let e = Errors.push e in
+    let e = CErrors.push e in
     handle_failure e vcs tty
 
-let print_ast id =
-  try
-    match VCS.visit id with
-    | { step = `Cmd { cast = { loc; expr } } }
-    | { step = `Fork (({ loc; expr }, _, _, _), _) } 
-    | { step = `Qed ({ qast = { loc; expr } }, _) } ->
-        let xml = 
-          try Texmacspp.tmpp expr loc
-          with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
-        xml;
-    | _ -> Xml_datatype.PCData "ERROR"
-  with _ -> Xml_datatype.PCData "ERROR"
+let get_ast id =
+  match VCS.visit id with
+  | { step = `Cmd { cast = { loc; expr } } }
+  | { step = `Fork (({ loc; expr }, _, _, _), _) } 
+  | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+         Some (expr, loc)
+  | _ -> None
 
 let stop_worker n = Slaves.cancel_worker n
 
+(* You may need to know the len + indentation of previous command to compute
+ * the indentation of the current one.
+ *  Eg.   foo. bar.
+ * Here bar is indented of the indentation of foo + its strlen (4) *)
+let ind_len_of id =
+  if Stateid.equal id Stateid.initial then 0
+  else match (VCS.visit id).step with
+  | `Cmd { ctac = true; cast = { indentation; strlen } } ->
+       indentation + strlen
+  | _ -> 0
+
 let add ~ontop ?newtip ?(check=ignore) verb eid s =
   let cur_tip = VCS.cur_tip () in
-  if Stateid.equal ontop cur_tip then begin
-    let _, ast as loc_ast = vernac_parse ?newtip eid s in
-    check(loc_ast);
-    let clas = classify_vernac ast in
-    match process_transaction ?newtip ~tty:false verb clas loc_ast with
-    | `Ok -> VCS.cur_tip (), `NewTip
-    | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
-  end else begin
+  if not (Stateid.equal ontop cur_tip) then
     (* For now, arbitrary edits should be announced with edit_at *)
-    anomaly(str"Not yet implemented, the GUI should not try this")
-  end
+    anomaly(str"Not yet implemented, the GUI should not try this");
+  let indentation, strlen, loc, ast =
+    vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
+  CWarnings.set_current_loc loc;
+  check(loc,ast);
+  let clas = classify_vernac ast in
+  let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
+  match process_transaction ?newtip ~tty:false aast clas with
+  | `Ok -> VCS.cur_tip (), `NewTip
+  | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
 
 let set_perspective id_list = Slaves.set_perspective id_list
 
@@ -2312,20 +2665,21 @@ type focus = {
   tip : Stateid.t
 }
 
-let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
+let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
     let newtip, route = report_with in
-    let _, ast as loc_ast = vernac_parse ~newtip ~route 0 s in
+    let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
+    CWarnings.set_current_loc loc;
     let clas = classify_vernac ast in
+    let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
     match clas with
     | VtStm (w,_), _ ->
-       ignore(process_transaction
-         ~tty:false true (VtStm (w,false), VtNow) loc_ast)
+       ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
     | _ ->
        ignore(process_transaction
-         ~tty:false true (VtQuery (false,report_with), VtNow) loc_ast))
+         ~tty:false aast (VtQuery (false,report_with), VtNow)))
   s
 
 let edit_at id =
@@ -2350,7 +2704,7 @@ let edit_at id =
     | _ -> assert false
   in
   let is_ancestor_of_cur_branch id =
-    Vcs_.NodeSet.mem id
+    Stateid.Set.mem id
       (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
   let has_failed qed_id =
     match VCS.visit qed_id with
@@ -2365,13 +2719,13 @@ let edit_at id =
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip old_branch =
     let master_id, cancel_switch, keep =
-      (* Hum, this should be the real start_id in the clusted and not next *)
+      (* Hum, this should be the real start_id in the cluster and not next *)
       match VCS.visit qed_id with
       | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
-      | _ -> anomaly (str "Cluster not ending with Qed") in
+      | _ -> anomaly (str "ProofTask not ending with Qed") in
     VCS.branch ~root:master_id ~pos:id
       VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
-    VCS.delete_cluster_of id;
+    VCS.delete_boxes_of id;
     cancel_switch := true;
     Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
@@ -2385,14 +2739,14 @@ let edit_at id =
     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
+         Stateid.Set.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
       (Option.default brname bn)
       (no_edit brinfo.VCS.kind);
-    VCS.delete_cluster_of id;
+    VCS.delete_boxes_of id;
     VCS.gc ();
     VCS.print ();
     if not !Flags.async_proofs_full then
@@ -2407,14 +2761,14 @@ let edit_at id =
         | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn)
         | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn)
         | _ -> None in
-      match focused, VCS.cluster_of id, branch_info with
+      match focused, VCS.proof_task_box_of id, branch_info with
       | _, Some _, None -> assert false
-      | false, Some (qed_id,start), Some(mode,bn) ->
+      | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
           let tip = VCS.cur_tip () in
           if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
           then reopen_branch start id mode qed_id tip bn
           else backto id (Some bn)
-      | true, Some (qed_id,_), Some(mode,bn) ->
+      | true, Some { qed = qed_id }, Some(mode,bn) ->
           if on_cur_branch id then begin
             assert false
           end else if is_ancestor_of_cur_branch id then begin
@@ -2439,14 +2793,14 @@ let edit_at id =
     VCS.print ();
     rc
   with e ->
-    let (e, info) = Errors.push e in
+    let (e, info) = CErrors.push e in
     match Stateid.get info with
     | None ->
         VCS.print ();
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
-          Errors.print_no_report e)
+          CErrors.print_no_report e)
     | Some (_, id) ->
-        prerr_endline ("Failed at state " ^ Stateid.to_string id);
+        prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         iraise (e, info)
@@ -2457,9 +2811,10 @@ let restore d = VCS.restore d
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
-let interp verb (_,e as lexpr) =
+let interp verb (loc,e) =
   let clas = classify_vernac e in
-  let rc = process_transaction ~tty:true verb clas lexpr in
+  let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in
+  let rc = process_transaction ~tty:true aast clas in
   if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
   if interactive () = `Yes ||
      (!Flags.async_proofs_mode = Flags.APoff &&
@@ -2472,7 +2827,7 @@ let interp verb (_,e as lexpr) =
        | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
-      let e = Errors.push e in
+      let e = CErrors.push e in
       handle_failure e vcs true
 
 let finish () = finish ()
diff --git a/stm/stm.mli b/stm/stm.mli
index ad89eb71..b8a2a385 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -9,6 +9,7 @@
 open Vernacexpr
 open Names
 open Feedback
+open Loc
 
 (** state-transaction-machine interface *)
 
@@ -19,7 +20,9 @@ open Feedback
    The sentence [s] is parsed in the state [ontop].
    If [newtip] is provided, then the returned state id is guaranteed to be
    [newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) ->
+val add :
+  ontop:Stateid.t -> ?newtip:Stateid.t ->
+  ?check:(vernac_expr located -> unit) ->
   bool -> edit_id -> string ->
     Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
@@ -75,7 +78,9 @@ val get_current_state : unit -> Stateid.t
 
 (* Misc *)
 val init : unit -> unit
-val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* This returns the node at that position *)
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
@@ -93,6 +98,82 @@ module ProofTask : AsyncTaskQueue.Task
 module TacTask   : AsyncTaskQueue.Task
 module QueryTask : AsyncTaskQueue.Task
 
+(** document structure customization *************************************** **)
+
+(* A proof block delimiter defines a syntactic delimiter for sub proofs
+   that, when contain an error, do not impact the rest of the proof.
+   While checking a proof, if an error occurs in a (valid) block then
+   processing can skip the entire block and go on to give feedback
+   on the rest of the proof.
+  
+   static_block_detection and dynamic_block_validation are run when
+   the closing block marker is parsed/executed respectively.
+  
+   static_block_detection is for example called when "}" is parsed and
+   declares a block containing all proof steps between it and the matching
+   "{".
+  
+   dynamic_block_validation is called when an error "crosses" the "}" statement.
+   Depending on the nature of the goal focused by "{" the block may absorb the
+   error or not.  For example if the focused goal occurs in the type of
+   another goal, then the block is leaky.
+   Note that one can design proof commands that need no dynamic validation.
+  
+   Example of document:
+
+      .. { tac1. tac2. } ..
+
+   Corresponding DAG:
+
+      .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
+                       
+   Declaration of block  [-------------------------------------------]
+
+      start = 5            the first state_id that could fail in the block
+      stop = 7             the node that may absorb the error
+      dynamic_switch = 4   dynamic check on this node
+      carry_on_data = ()   no need to carry extra data from static to dynamic
+                           checks
+*)
+
+module DynBlockData : Dyn.S
+
+type static_block_declaration = {
+  block_start : Stateid.t;
+  block_stop : Stateid.t;
+  dynamic_switch : Stateid.t;
+  carry_on_data : DynBlockData.t;
+}
+
+type document_node = {
+  indentation : int;
+  ast : Vernacexpr.vernac_expr;
+  id : Stateid.t;
+}
+
+type document_view = {
+  entry_point : document_node;
+  prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+  document_view -> static_block_declaration option
+
+type recovery_action = {
+  base_state : Stateid.t;
+  goals_to_admit : Goal.goal list;
+  recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+val register_proof_block_delimiter :
+  Vernacexpr.proof_block_name ->
+  static_block_detection ->
+  dynamic_block_error_recovery ->
+    unit
+
 (** customization ********************************************************** **)
 
 (* From the master (or worker, but beware that to install the hook
@@ -119,14 +200,15 @@ type state = {
   proof : Proof_global.state;
   shallow : bool
 }
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
+val state_of_id :
+  Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
 
 (** 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
+   [finish] is called as the last bit of this function if the system
    is running interactively (-emacs or coqtop). *)
-val interp : bool -> located_vernac_expr -> unit
+val interp : bool -> vernac_expr located -> unit
 
 (* Queries for backward compatibility *)
 val current_proof_depth : unit -> int
@@ -134,7 +216,7 @@ 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 *)
+(* Hooks to be set by other Coq components in order to break file cycles *)
 val process_error_hook : Future.fix_exn Hook.t
 val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
   Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869..939ee187 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,6 @@ Vernac_classifier
 Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
-Texmacspp
 Stm
+ProofBlockDelimiter
 Vio_checking
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index ee121c46..a0b08778 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -87,7 +87,7 @@ let broadcast { lock = m; cond = c } =
   Mutex.unlock m
 
 let push { queue = q; lock = m; cond = c; release } x =
-  if release then Errors.anomaly(Pp.str
+  if release then CErrors.anomaly(Pp.str
     "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
   Mutex.lock m;
   PriorityQueue.push q x;
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
deleted file mode 100644
index 85cb4570..00000000
--- a/stm/texmacspp.ml
+++ /dev/null
@@ -1,770 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-
-let unlock loc =
-  let start, stop = Loc.unloc loc in
-  (string_of_int start, string_of_int stop)
-
-let xmlNoop = (* almost noop  *)
-  PCData ""
-
-let xmlWithLoc loc ename attr xml =
-  let start, stop = unlock loc in
-  Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
-
-let get_fst_attr_in_xml_list attr xml_list =
-  let attrs_list =
-    List.map (function
-      | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
-      | _ -> [])
-    xml_list in
-  match List.flatten attrs_list with
-  | [] -> (attr, "")
-  | l  -> (List.hd l)
-
-let backstep_loc xmllist =
-  let start_att = get_fst_attr_in_xml_list "begin" xmllist in
-  let stop_att =  get_fst_attr_in_xml_list "end" (List.rev xmllist) in
-  [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
-  let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
-  let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
-  match att1, att2 with
-  | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
-  | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
-  | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
-  | _ -> 0
-
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
-
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
-
-let xmlThm typ name loc xml =
-  xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef typ name loc xml =
-  xmlWithLoc loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation attr name loc xml =
-  xmlWithLoc loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation attr name loc =
-  xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst name ?(attr=[]) loc =
-  xmlWithLoc loc "constant" (("name", name) :: attr) []
-
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
-  xmlWithLoc loc "operator"
-    (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
-
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
-
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
-
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
-
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
-
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
-
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
-
-let xmlReference ref =
-  let name = Libnames.string_of_reference ref in
-  let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
-  let b, e = string_of_int i, string_of_int j in
-  Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
-
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
-
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
-
-let xmlScope loc action ?(attr=[]) name xml =
-  xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
-
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-
-let xmlRawTactic name rtac =
-  Element("rawtactic", ["name",name],
-    [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
-
-let xmlSectionSubsetDescr name ssd =
-  Element("sectionsubsetdescr",["name",name],
-    [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule loc s =
-  xmlWithLoc loc "declarexmlmodule" []
-    (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
-
-let xmlTODO loc x =
-  xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
-  match n with
-  | Anonymous -> "_"
-  | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
-  match s with
-  | GProp -> "Prop"
-  | GSet -> "Set"
-  | GType _ -> "Type"
-
-let string_of_cast_sort c =
-  match c with
-  | CastConv _ -> "CastConv"
-  | CastVM _ -> "CastVM"
-  | CastNative _ -> "CastNative"
-  | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
-  match s with
-  | LetStyle -> "Let"
-  | IfStyle -> "If"
-  | LetPatternStyle -> "LetPattern"
-  | MatchStyle -> "Match"
-  | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
-  | SetItemLevel (sl, NumLevel n) ->
-      List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
-  | SetItemLevel (sl, NextLevel) ->
-      List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
-  | SetLevel i -> ["level", string_of_int i]
-  | SetAssoc a ->
-      begin match a with
-      | NonA -> ["",""]
-      | RightA -> ["associativity", "right"]
-      | LeftA -> ["associativity", "left"]
-      end
-  | SetEntryType (s, _) -> ["entrytype", s]
-  | SetOnlyParsing v -> ["compat", Flags.pr_version v]
-  | SetFormat (system, (loc, s)) ->
-      let start, stop = unlock loc in
-      ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
-  match l, a, many with
-  | (Discharge, Logical,      true)  -> "Hypotheses"
-  | (Discharge, Logical,      false) -> "Hypothesis"
-  | (Discharge, Definitional, true)  -> "Variables"
-  | (Discharge, Definitional, false) -> "Variable"
-  | (Global,    Logical,      true)  -> "Axioms"
-  | (Global,    Logical,      false) -> "Axiom"
-  | (Global,    Definitional, true)  -> "Parameters"
-  | (Global,    Definitional, false) -> "Parameter"
-  | (Local,     Logical,      true)  -> "Local Axioms"
-  | (Local,     Logical,      false) -> "Local Axiom"
-  | (Local,     Definitional, true)  -> "Local Parameters"
-  | (Local,     Definitional, false) -> "Local Parameter"
-  | (Global,    Conjectural, _)      -> "Conjecture"
-  | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
-  let tlist =
-    List.flatten
-        (List.map
-          (fun (loc_names, _, e) ->
-            let names =
-              (List.map
-                (fun (loc, name) ->
-                  xmlCst (string_of_name name) loc) loc_names) in
-            match e with
-              | CHole _ -> names
-              | _ -> names @ [pp_expr e])
-          bl) in
-  match tlist with
-    | [e] -> e
-    | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
-  Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
-  match lb with
-  | LocalRawDef ((_, nam), ce) ->
-      let attrs = ["name", string_of_name nam] in
-      pp_expr ~attr:attrs ce
-  | LocalRawAssum (namll, _, ce) ->
-      let ppl =
-        List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
-      xmlTyped (ppl @ [pp_expr ce])
-and pp_local_decl_expr lde = (* don't know what it is for now *)
-  match lde with
-  | AssumExpr (_, ce) -> pp_expr ce
-  | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
-  (* inductive_expr *)
-  let b,e = Loc.unloc l in
-  let location = ["begin", string_of_int b; "end", string_of_int e] in
-  [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
-  begin match cl_or_rdexpr with
-  | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
-  | RecordDecl (_, ldewwwl) ->
-      List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
-  end @
-  begin match ceo with (* don't know what it is for now *)
-  | Some ce -> [pp_expr ce]
-  | None -> []
-  end @
-  (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
-  let attrs =
-    match optid with
-    | None -> []
-    | Some (loc, id) ->
-        let start, stop = unlock loc in
-        ["begin", start; "end", stop ; "name", Id.to_string id] in
-  let kind, expr =
-    match roe with
-    | CStructRec -> "struct", []
-    | CWfRec e -> "rec", [pp_expr e]
-    | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
-    | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
-  Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
-  (* fixpoint_expr *)
-  let start, stop = unlock loc in
-  let id = Id.to_string id in
-  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
-  (* fixpoint name *)
-  [pp_recursion_order_expr optid roe] @
-  (List.map pp_local_binder lbl) @
-  [pp_expr ce] @
-  begin match ceo with (* don't know what it is for now *)
-  | Some ce -> [pp_expr ce]
-  | None -> []
-  end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
-  (* Nota: it is like fixpoint_expr without (optid, roe)
-   * so could be merged if there is no more differences *)
-  let start, stop = unlock loc in
-  let id = Id.to_string id in
-  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
-  (* cofixpoint name *)
-  (List.map pp_local_binder lbl) @
-  [pp_expr ce] @
-  begin match ceo with (* don't know what it is for now *)
-  | Some ce -> [pp_expr ce]
-  | None -> []
-  end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
-  match cpe with
-  | CPatAlias (loc, cpe, id) ->
-      xmlApply loc
-        (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
-          [pp_cases_pattern_expr cpe])
-  | CPatCstr (loc, ref, cpel1, cpel2) ->
-      xmlApply loc
-        (xmlOperator "reference"
-           ~attr:["name", Libnames.string_of_reference ref] loc ::
-         [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
-          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatAtom (loc, optr) ->
-      let attrs = match optr with
-        | None -> []
-        | Some r -> ["name", Libnames.string_of_reference r] in
-      xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
-  | CPatOr (loc, cpel) ->
-      xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
-  | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
-      xmlApply loc
-        (xmlOperator "notation" loc ::
-          [xmlOperator n loc;
-           Element ("subst", [],
-             [Element ("subterms", [],
-                List.map pp_cases_pattern_expr subst_constr);
-              Element ("recsubterms", [],
-                List.map
-                  (fun (cpel) ->
-                     Element ("recsubterm", [],
-                       List.map pp_cases_pattern_expr cpel))
-                subst_rec)]);
-           Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
-  | CPatPrim (loc, tok) -> pp_token loc tok
-  | CPatRecord (loc, rcl) ->
-      xmlApply loc
-        (xmlOperator "record" loc ::
-           List.map (fun (r, cpe) ->
-             Element ("field",
-               ["reference", Libnames.string_of_reference r],
-               [pp_cases_pattern_expr cpe]))
-           rcl)
-  | CPatDelimiters (loc, delim, cpe) ->
-      xmlApply loc
-        (xmlOperator "delimiter" ~attr:["name", delim] loc ::
-          [pp_cases_pattern_expr cpe])
-and pp_case_expr (e, (name, pat)) =
-  match name, pat with
-  | None, None -> xmlScrutinee [pp_expr e]
-  | Some (loc, name), None ->
-      let start, stop= unlock loc in
-      xmlScrutinee ~attr:["name", string_of_name name;
-                          "begin", start; "end", stop] [pp_expr e]
-  | Some (loc, name), Some p ->
-      let start, stop= unlock loc in
-      xmlScrutinee ~attr:["name", string_of_name name;
-                          "begin", start; "end", stop]
-        [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-  | None, Some p ->
-      xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
-  xmlWith
-    (List.map
-      (fun (_, cpel, e) ->
-        let ppcepl =
-          List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
-        let ppe = [pp_expr e] in
-        xmlCase (ppcepl @ ppe))
-     bel)
-and pp_token loc tok =
-  let tokstr =
-    match tok with
-    | String s -> PCData s
-    | Numeral n -> PCData (to_string n) in
-  xmlToken loc [tokstr]
-and pp_local_binder_list lbl =
-  let l = (List.map pp_local_binder lbl) in
-  Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
-  let l = List.map pp_expr cel in
-  Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
-  match e with
-  | CRef (r, _) ->
-      xmlCst ~attr
-        (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
-  | CProdN (loc, bl, e) ->
-      xmlApply loc
-        (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
-  | CApp (loc, (_, hd), args) ->
-       xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
-  | CAppExpl (loc, (_, r, _), args) ->
-       xmlApply ~attr loc
-         (xmlCst (Libnames.string_of_reference r)
-                 (Libnames.loc_of_reference r) :: List.map pp_expr args)
-  | CNotation (loc, notation,  ([],[],[])) ->
-       xmlOperator notation loc
-  | CNotation (loc, notation,  (args, cell, lbll)) ->
-      let fmts = Notation.find_notation_extra_printing_rules notation in
-      let oper = xmlOperator notation loc ~pprules:fmts in
-      let cels = List.map pp_const_expr_list cell in
-      let lbls = List.map pp_local_binder_list lbll in
-      let args = List.map pp_expr args in
-      xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
-  | CSort(loc, s) ->
-      xmlOperator (string_of_glob_sort s) loc
-  | CDelimiters (loc, scope, ce) ->
-      xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
-        [pp_expr ce])
-  | CPrim (loc, tok) -> pp_token loc tok
-  | CGeneralization (loc, kind, _, e) ->
-      let kind= match kind with
-      | Explicit -> "explicit"
-      | Implicit -> "implicit" in
-      xmlApply loc
-        (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
-  | CCast (loc, e, tc) ->
-      begin match tc with
-      | CastConv t | CastVM t |CastNative t ->
-          xmlApply loc
-            (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
-             [pp_expr e; pp_expr t])
-      | CastCoerce   ->
-          xmlApply loc
-            (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
-             [pp_expr e])
-      end
-  | CEvar (loc, ek, cel) ->
-      let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
-      xmlApply loc
-        (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
-          ppcel)
-  | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
-  | CHole (loc, _, _, _) -> xmlCst ~attr  "_" loc
-  | CIf (loc, test, (_, ret), th, el) ->
-      let return = match ret with
-      | None -> []
-      | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply loc
-        (xmlOperator "if" loc ::
-          return @ [pp_expr th] @ [pp_expr el])
-  | CLetTuple (loc, names, (_, ret), value, body) ->
-      let return = match ret with
-      | None -> []
-      | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply loc
-        (xmlOperator "lettuple" loc ::
-          return @
-          (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
-          [pp_expr value; pp_expr body])
-  | CCases (loc, sty, ret, cel, bel) ->
-      let return = match ret with
-      | None -> []
-      | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply loc
-        (xmlOperator "match" loc  ~attr:["style", (string_of_case_style sty)] ::
-          (return @
-           [Element ("scrutinees", [], List.map pp_case_expr cel)] @
-           [pp_branch_expr_list bel]))
-  | CRecord (_, _, _) -> assert false
-  | CLetIn (loc, (varloc, var), value, body) ->
-      xmlApply loc
-        (xmlOperator "let" loc ::
-         [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
-  | CLambdaN (loc, bl, e) ->
-      xmlApply loc
-        (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
-  | CCoFix (_, _, _) -> assert false
-  | CFix (loc, lid, fel) ->
-      xmlApply loc
-        (xmlOperator "fix" loc ::
-           List.flatten (List.map
-             (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
-             fel))
-
-let pp_comment (c) =
-  match c with
-  | CommentConstr e -> [pp_expr e]
-  | CommentString s -> [Element ("string", [], [PCData s])]
-  | CommentInt i -> [PCData (string_of_int i)]
-
-let rec tmpp v loc =
-  match v with
-  (* Control *)
-  | VernacLoad (verbose,f) ->
-      xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
-  | VernacTime l ->
-      xmlApply loc (Element("time",[],[]) ::
-                    List.map (fun(loc,e) ->tmpp e loc) l)
-  | VernacRedirect (s, l) ->
-      xmlApply loc (Element("redirect",["path", s],[]) ::
-                      List.map (fun(loc,e) ->tmpp e loc) l)
-  | VernacTimeout (s,e) ->
-      xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
-                    [tmpp e loc])
-  | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
-  | VernacError _ -> xmlWithLoc loc "error" [] []
-
-  (* Syntax *)
-  | VernacTacticNotation _ as x ->
-      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-  | VernacSyntaxExtension (_, ((_, name), sml)) ->
-      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      xmlReservedNotation attrs name loc
-
-  | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
-  | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
-  | VernacDelimiters (name,Some tag) ->
-      xmlScope loc "delimit" name ~attr:["delimiter",tag] []
-  | VernacDelimiters (name,None) ->
-      xmlScope loc "undelimit" name ~attr:[] []
-  | VernacBindScope (name,l) ->
-      xmlScope loc "bind" name
-        (List.map (function
-          | ByNotation(loc,name,None) -> xmlNotation [] name loc []
-          | ByNotation(loc,name,Some d) ->
-              xmlNotation ["delimiter",d] name loc []
-          | AN ref -> xmlReference ref) l)
-  | VernacInfix (_,((_,name),sml),ce,sn) ->
-      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      let sc_attr =
-        match sn with
-        | Some scope -> ["scope", scope]
-        | None -> [] in
-      xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
-  | VernacNotation (_, ce, (lstr, sml), sn) ->
-      let name = snd lstr in
-      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      let sc_attr =
-        match sn with
-        | Some scope -> ["scope", scope]
-        | None -> [] in
-      xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
-  | VernacNotationAddFormat _ as x -> xmlTODO loc x
-  | VernacUniverse _
-  | VernacConstraint _
-  | VernacPolymorphic (_, _) as x -> xmlTODO loc x
-  (* Gallina *)
-  | VernacDefinition (ldk, ((_,id),_), de) ->
-      let l, dk =
-        match ldk with
-        | Some l, dk -> (l, dk)
-        | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
-      let e =
-        match de with
-        | ProveBody (_, ce) -> ce
-        | DefineBody (_, Some _, ce, None) -> ce
-        | DefineBody (_, None  , ce, None) -> ce
-        | DefineBody (_, Some _, ce, Some _) -> ce
-        | DefineBody (_, None  , ce, Some _) -> ce in
-      let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
-      let str_id = Id.to_string id in
-      (xmlDef str_dk str_id loc [pp_expr e])
-  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
-      let str_tk = Kindops.string_of_theorem_kind tk in
-      let str_id = Id.to_string id in
-      (xmlThm str_tk str_id loc [pp_expr statement])
-  | VernacStartTheoremProof _ as x -> xmlTODO loc x
-  | VernacEndProof pe ->
-      begin
-        match pe with
-        | Admitted -> xmlQed loc
-        | Proved (_, Some ((_, id), Some tk)) ->
-            let nam = Id.to_string id in
-            let typ = Kindops.string_of_theorem_kind tk in
-            xmlQed ~attr:["name", nam; "type", typ] loc
-        | Proved (_, Some ((_, id), None)) ->
-            let nam = Id.to_string id in
-            xmlQed ~attr:["name", nam] loc
-        | Proved _ -> xmlQed loc
-      end
-  | VernacExactProof _ as x -> xmlTODO loc x
-  | VernacAssumption ((l, a), _, sbwcl) ->
-      let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
-      let many =
-        List.length (List.flatten (List.map fst binders)) > 1 in
-      let exprs =
-        List.flatten (List.map pp_simple_binder binders) in
-      let l = match l with Some x -> x | None -> Decl_kinds.Global in
-      let kind = string_of_assumption_kind l a many in
-      xmlAssumption kind loc exprs
-  | VernacInductive (_, _, iednll) ->
-      let kind =
-        let (_, _, _, k, _),_ = List.hd iednll in
-	  begin
-            match k with
-            | Record -> "Record"
-            | Structure -> "Structure"
-            | Inductive_kw -> "Inductive"
-            | CoInductive -> "CoInductive"
-            | Class _ -> "Class"
-            | Variant -> "Variant"
-          end in
-      let exprs =
-        List.flatten (* should probably not be flattened *)
-          (List.map
-            (fun (ie, dnl) -> (pp_inductive_expr ie) @
-                              (List.map pp_decl_notation dnl)) iednll) in
-      xmlInductive kind loc exprs
-  | VernacFixpoint (_, fednll) ->
-      let exprs =
-        List.flatten (* should probably not be flattened *)
-          (List.map
-            (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
-                              (List.map pp_decl_notation dnl)) fednll) in
-      xmlFixpoint exprs
-  | VernacCoFixpoint (_, cfednll) ->
-      (* Nota: it is like VernacFixpoint without so could be merged *)
-      let exprs =
-        List.flatten (* should probably not be flattened *)
-          (List.map
-            (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
-                              (List.map pp_decl_notation dnl)) cfednll) in
-      xmlCoFixpoint exprs
-  | VernacScheme _ as x -> xmlTODO loc x
-  | VernacCombinedScheme _ as x -> xmlTODO loc x
-
-  (* Gallina extensions *)
-  | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
-  | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
-  | VernacNameSectionHypSet _ as x -> xmlTODO loc x
-  | VernacRequire (from, import, l) ->
-      let import = match import with
-      | None -> []
-      | Some true -> ["export","true"]
-      | Some false -> ["import","true"]
-      in
-      let from = match from with
-      | None -> []
-      | Some r -> ["from", Libnames.string_of_reference r]
-      in
-      xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacImport (true,l) ->
-      xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacImport (false,l) ->
-      xmlImport loc (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacCanonical r ->
-      let attr =
-        match r with
-        | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
-        | AN (Ident (_, id)) -> ["id", Id.to_string id]
-        | ByNotation (_, s, _) -> ["notation", s] in
-      xmlCanonicalStructure attr loc
-  | VernacCoercion _ as x -> xmlTODO loc x
-  | VernacIdentityCoercion _ as x -> xmlTODO loc x
-
-  (* Type classes *)
-  | VernacInstance _ as x -> xmlTODO loc x
-
-  | VernacContext _ as x -> xmlTODO loc x
-
-  | VernacDeclareInstances _ as x -> xmlTODO loc x
-
-  | VernacDeclareClass _ as x -> xmlTODO loc x
-
-  (* Modules and Module Types *)
-  | VernacDeclareModule _ as x -> xmlTODO loc x
-  | VernacDefineModule _ as x -> xmlTODO loc x
-  | VernacDeclareModuleType _ as x -> xmlTODO loc x
-  | VernacInclude _ as x -> xmlTODO loc x
-
-  (* Solving *)
-
-  | (VernacSolve _ | VernacSolveExistential _) as x ->
-      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-  (* Auxiliary file and library management *)
-  | VernacAddLoadPath (recf,name,None) ->
-      xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
-  | VernacAddLoadPath (recf,name,Some dp) ->
-      xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
-        [PCData (Names.DirPath.to_string dp)]
-  | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
-  | VernacAddMLPath (recf,name) ->
-      xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
-  | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
-  | VernacChdir _ as x -> xmlTODO loc x
-
-  (* State management *)
-  | VernacWriteState _ as x -> xmlTODO loc x
-  | VernacRestoreState _ as x -> xmlTODO loc x
-
-  (* Resetting *)
-  | VernacResetName _ as x -> xmlTODO loc x
-  | VernacResetInitial as x -> xmlTODO loc x
-  | VernacBack _ as x -> xmlTODO loc x
-  | VernacBackTo _ -> PCData "VernacBackTo"
-
-  (* Commands *)
-  | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
-  | VernacCreateHintDb _ as x -> xmlTODO loc x
-  | VernacRemoveHints _ as x -> xmlTODO loc x
-  | VernacHints _ as x -> xmlTODO loc x
-  | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
-      let name = Id.to_string name in
-      let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
-      xmlNotation attrs name loc [pp_expr ce]
-  | VernacDeclareImplicits _ as x -> xmlTODO loc x
-  | VernacArguments _ as x -> xmlTODO loc x
-  | VernacArgumentsScope _ as x -> xmlTODO loc x
-  | VernacReserve _ as x -> xmlTODO loc x
-  | VernacGeneralizable _ as x -> xmlTODO loc x
-  | VernacSetOpacity _ as x -> xmlTODO loc x
-  | VernacSetStrategy _ as x -> xmlTODO loc x
-  | VernacUnsetOption _ as x -> xmlTODO loc x
-  | VernacSetOption _ as x -> xmlTODO loc x
-  | VernacAddOption _ as x -> xmlTODO loc x
-  | VernacRemoveOption _ as x -> xmlTODO loc x
-  | VernacMemOption _ as x -> xmlTODO loc x
-  | VernacPrintOption _ as x -> xmlTODO loc x
-  | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
-  | VernacGlobalCheck _ as x -> xmlTODO loc x
-  | VernacDeclareReduction _ as x -> xmlTODO loc x
-  | VernacPrint _ as x -> xmlTODO loc x
-  | VernacSearch _ as x -> xmlTODO loc x
-  | VernacLocate _ as x -> xmlTODO loc x
-  | VernacRegister _ as x -> xmlTODO loc x
-  | VernacComments (cl) ->
-      xmlComment loc (List.flatten (List.map pp_comment cl))
-  | VernacNop as x -> xmlTODO loc x
-
-  (* Stm backdoor *)
-  | VernacStm _ as x -> xmlTODO loc x
-
-  (* Proof management *)
-  | VernacGoal _ as x -> xmlTODO loc x
-  | VernacAbort _ as x -> xmlTODO loc x
-  | VernacAbortAll -> PCData "VernacAbortAll"
-  | VernacRestart as x -> xmlTODO loc x
-  | VernacUndo _ as x -> xmlTODO loc x
-  | VernacUndoTo _ as x -> xmlTODO loc x
-  | VernacBacktrack _ as x -> xmlTODO loc x
-  | VernacFocus _ as x -> xmlTODO loc x
-  | VernacUnfocus as x -> xmlTODO loc x
-  | VernacUnfocused as x -> xmlTODO loc x
-  | VernacBullet _ as x -> xmlTODO loc x
-  | VernacSubproof _ as x -> xmlTODO loc x
-  | VernacEndSubproof as x -> xmlTODO loc x
-  | VernacShow _ as x -> xmlTODO loc x
-  | VernacCheckGuard as x -> xmlTODO loc x
-  | VernacProof (tac,using) ->
-      let tac = Option.map (xmlRawTactic "closingtactic") tac in
-      let using = Option.map (xmlSectionSubsetDescr "using") using in
-      xmlProof loc (Option.List.(cons tac (cons using [])))
-  | VernacProofMode name -> xmlProofMode loc name
-
-  (* Toplevel control *)
-  | VernacToplevelControl _ as x -> xmlTODO loc x
-
-  (* For extension *)
-  | VernacExtend _ as x ->
-      xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-  (* Flags *)
-  | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
-  | VernacLocal (b,e) ->
-      xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
-                    [tmpp e loc])
-
-let tmpp v loc =
-  match tmpp v loc with
-  | Element("ltac",_,_) as x -> x
-  | xml -> xmlGallina loc [xml]
diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli
deleted file mode 100644
index 858847fb..00000000
--- a/stm/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/stm/vcs.ml b/stm/vcs.ml
index 38c02990..d3886464 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 
 module type S = sig
 
@@ -22,51 +22,49 @@ module type S = sig
   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
+  
+  type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ]
+  
+  val empty : id -> ('kind,'diff,'info,'property_data) t
+  
+  val current_branch : ('k,'e,'i,'c) t -> Branch.t
+  val branches : ('k,'e,'i,'c) t -> Branch.t list
+  
+  val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) 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
+    ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id ->
+        Branch.t -> 'kind -> ('kind,'e,'i,'c) t
+  val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) 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
+    ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i,'c) t
+  val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) 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
+    ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+            Branch.t -> ('k,'diff,'i,'c) t
+  val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
   
-  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
+  val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
+  val get_info : ('k,'e,'info,'c) t -> id -> 'info option
 
+  (* Read only dag *)
   module Dag : Dag.S with type node = id
-  val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t
+  val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
+
+  val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
+  val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
+  val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t 
 
-  val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
-  val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
-  val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t 
+  (* Removes all unreachable nodes and returns them *)
+  val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
+  val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
 
 end
 
@@ -78,7 +76,6 @@ type id = OT.t
 
 module NodeSet = Dag.NodeSet
 
-
 module Branch =
 struct
   type t = string
@@ -99,10 +96,10 @@ type 'kind branch_info = {
   pos  : id;
 }
 
-type ('kind,'edge,'info) t = {
+type ('kind,'edge,'info,'property_data) t = {
   cur_branch   : Branch.t;
   heads        : 'kind branch_info BranchMap.t;
-  dag          : ('edge,'info,id*id) Dag.t;
+  dag          : ('edge,'info,'property_data) Dag.t;
 }
 
 let empty root = {
@@ -167,9 +164,9 @@ 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 create_property vcs l i = { vcs with dag = Dag.create_property vcs.dag l i }
+let property_of vcs i = Dag.property_of vcs.dag i
+let delete_property vcs c = { vcs with dag = Dag.del_property vcs.dag c }
 
 let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
 let dag vcs = vcs.dag
diff --git a/stm/vcs.mli b/stm/vcs.mli
index 8f22fee8..46b40f8a 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -19,10 +19,11 @@
    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:
+   The type [Vcs.t] has 4 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)
+    ['cdata] extra data hold by dag properties
 *)
 
 module type S = sig
@@ -45,46 +46,51 @@ module type S = sig
     pos  : id;
   }
   
-  type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
+  type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ]
   
-  val empty : id -> ('kind,'diff,'info) t
+  val empty : id -> ('kind,'diff,'info,'property_data) t
   
-  val current_branch : ('k,'e,'i) t -> Branch.t
-  val branches : ('k,'e,'i) t -> Branch.t list
+  val current_branch : ('k,'e,'i,'c) t -> Branch.t
+  val branches : ('k,'e,'i,'c) 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 get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) 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
+    ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id ->
+        Branch.t -> 'kind -> ('kind,'e,'i,'c) t
+  val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) 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
+    ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i,'c) t
+  val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) 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
+    ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+            Branch.t -> ('k,'diff,'i,'c) t
+  val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
   
-  val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
-  val get_info : ('k,'e,'info) t -> id -> 'info option
+  val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
+  val get_info : ('k,'e,'info,'c) t -> id -> 'info option
 
-  module NodeSet : Set.S with type elt = id
+  (* Read only dag *)
+  module Dag : Dag.S with type node = id
+  val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
   
-  (* Removes all unreachable nodes and returns them *)
-  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+  (* Properties are not a concept typical of a VCS, but a useful metadata
+   * of a DAG (or graph). *)
+  val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
+  val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
+  val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t 
 
-  val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+  (* Removes all unreachable nodes and returns them *)
+  val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
+  val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
 
-  (* read only dag *)
-  module Dag : Dag.S with type node = id
-  val dag : ('kind,'diff,'info) t -> ('diff,'info,id * id) Dag.t
  
-  val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
-  val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
-  val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t 
-
 end
 
-module Make(OT : Map.OrderedType) : S with type id = OT.t
+module Make(OT : Map.OrderedType) : S
+with type id = OT.t
+and type Dag.node = OT.t
+and type Dag.NodeSet.t = Set.Make(OT).t
+and type Dag.NodeSet.elt = OT.t
+
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index edb54ece..dc5be08a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -7,11 +7,18 @@
 (************************************************************************)
 
 open Vernacexpr
-open Errors
+open CErrors
 open Pp
 
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
 let string_of_in_script b = if b then " (inside script)" else ""
 
+let string_of_parallel = function
+  | `Yes (solve,abs) ->
+       "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
+  | `No -> ""
+
 let string_of_vernac_type = function
   | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
@@ -19,8 +26,9 @@ let string_of_vernac_type = function
   | VtQed VtKeep -> "Qed(keep)"
   | VtQed VtKeepAsAxiom -> "Qed(admitted)"
   | VtQed VtDrop -> "Qed(drop)"
-  | VtProofStep false -> "ProofStep"
-  | VtProofStep true -> "ProofStep (parallel)"
+  | VtProofStep { parallel; proof_block_detection } ->
+      "ProofStep " ^ string_of_parallel parallel ^
+        Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
   | VtQuery (b,(id,route)) ->
       "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
@@ -60,7 +68,7 @@ let undo_classifier = ref (fun _ -> assert false)
 let set_undo_classifier f = undo_classifier := f
 
 let rec classify_vernac e =
-  let rec static_classifier e = match e with
+  let static_classifier e = match e with
     (* PG compatibility *)
     | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
     | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
@@ -86,12 +94,14 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
+    | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
           | VtStm _ | VtProofMode _ ), _ as x -> x
-        | VtQed _, _ -> VtProofStep false, VtNow
+        | VtQed _, _ ->
+            VtProofStep { parallel = `No; proof_block_detection = None },
+            VtNow
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
@@ -102,42 +112,47 @@ let rec classify_vernac e =
     | VernacCheckMayEval _ ->
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
-    | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
     | VernacProof _ 
-    | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
-    | VernacSubproof _ | VernacEndSubproof
-    | VernacSolve _ 
+    | VernacSubproof _
     | VernacCheckGuard
     | VernacUnfocused
-    | VernacSolveExistential _ -> VtProofStep false, VtLater
+    | VernacSolveExistential _ ->
+        VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
+    | VernacBullet _ ->
+        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
+        VtLater
+    | VernacEndSubproof -> 
+        VtProofStep { parallel = `No;
+                      proof_block_detection = Some "curly" },
+        VtLater
     (* Options changing parser *)
     | VernacUnsetOption (["Default";"Proof";"Using"])
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition (
        (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
-        VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+        VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
-        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+        VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
-        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
-    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+        VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+    | VernacGoal _ -> VtStartProof (default_proof_mode (),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
+        then VtStartProof (default_proof_mode (),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
+        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
@@ -166,7 +181,7 @@ let rec classify_vernac e =
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacUnsetOption _ | VernacSetOption _
+    | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _
     | VernacAddOption _ | VernacRemoveOption _
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _
@@ -175,11 +190,6 @@ let rec classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
-    | VernacDeclareTacticDefinition (_,l) ->
-        let open Libnames in
-        VtSideff (List.map (function
-          | (Ident (_,r),_,_) -> r
-          | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
@@ -195,7 +205,6 @@ let rec classify_vernac e =
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _ 
     | VernacSyntacticDefinition _
-    | VernacTacticNotation _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
@@ -208,7 +217,6 @@ let rec classify_vernac e =
     | VernacResetName _ | VernacResetInitial
     | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
     (* What are these? *)
-    | VernacNop
     | VernacToplevelControl _
     | VernacRestoreState _
     | VernacWriteState _ -> VtUnknown, VtNow
@@ -217,13 +225,6 @@ let rec classify_vernac e =
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
-  and classify_vernac_list = function
-    (* spiwack: It would be better to define a monoid on classifiers.
-       So that the classifier of the list would be the composition of
-       the classifier of the individual commands. Currently: special
-       case for singleton lists.*)
-    | [_,c] -> static_classifier c
-    | l -> VtUnknown,VtNow
   in
   let res = static_classifier e in
     if Flags.is_universe_polymorphism () then
@@ -233,4 +234,4 @@ let rec classify_vernac e =
 let classify_as_query =
   VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
 let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep false, VtLater
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index d4dcf72c..a6237daa 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -24,7 +24,7 @@ end
 module Pool = Map.Make(IntOT)
 
 let schedule_vio_checking j fs =
-  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
@@ -98,7 +98,7 @@ let schedule_vio_checking j fs =
   exit !rc
 
 let schedule_vio_compilation j fs =
-  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  if j < 1 then CErrors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index b94fae54..9623765d 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -52,7 +52,7 @@ let master_handshake worker_id ic oc =
       Printf.eprintf "Handshake with %s failed: protocol mismatch\n" worker_id;
       exit 1;
     end
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     Printf.eprintf "Handshake with %s failed: %s\n"
       worker_id (Printexc.to_string e);
     exit 1
@@ -65,7 +65,7 @@ let worker_handshake slave_ic slave_oc =
       exit 1;
     end;
     Marshal.to_channel slave_oc v []; flush slave_oc;
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
     exit 1