Merge remote-tracking branch 'origin/pr/173' into trunk

This is the "error resiliency" mode for STM

23 files changed, 1088 insertions, 329 deletions

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7cf500400..ebd11c168 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -46,6 +46,43 @@ proof does not begin with \texttt{Proof using}, the system records in an
 auxiliary file, produced along with the \texttt{.vo} file, the list of
 section variables used.
 
+\section{Proof blocks and error resilience}
+
+Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq
+is able to completely check a document containing errors instead of bailing
+out at the first failure.
+
+Two kind of errors are supported: errors occurring in vernacular commands and
+errors occurring in proofs.
+
+To properly recover from a failing tactic, Coq needs to recognize the structure of
+the proof in order to confine the error to a sub proof.  Proof block detection
+is performed by looking at the syntax of the proof script (i.e. also looking at indentation).
+Coq comes with four kind of proof blocks, and an ML API to add new ones.
+
+\begin{description}
+\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling}
+\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector
+\item[indent] blocks end with a tactic indented less than the previous one
+\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level
+\end{description}
+
+\subsection{Caveats}
+
+When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by
+the first error.  Error resiliency for vernacular commands can be switched off passing
+\texttt{-async-proofs-command-error-resilience off} to CoqIDE.
+
+An incorrect proof block detection can result into an incorrect error recovery and
+hence in bogus errors.  Proof block detection cannot be precise for bullets or
+any other non well parenthesized proof structure.  Error resiliency can be
+turned off or selectively activated for any set of block kind passing to
+CoqIDE one of the following options:
+\texttt{-async-proofs-tactic-error-resilience off},
+\texttt{-async-proofs-tactic-error-resilience all},
+\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}.
+Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. 
+
 \subsubsection{Automatic suggestion of proof annotations}
 
 The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7996b7969..93ba55c61 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -303,6 +303,9 @@ val guard_no_unifiable : Names.Name.t list option tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
+(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
+val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
+
 (** [with_shelf tac] executes [tac] and returns its result together with the set
     of goals shelved by [tac]. The current shelf is unchanged. *)
 val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 930135995..6ffe771da 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -741,7 +741,7 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC");
+(*           if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
           messages#push Feedback.Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ae9328fcc..6ce15a7c5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -454,7 +454,7 @@ type vernac_type =
   | VtStartProof of vernac_start
   | VtSideff of vernac_sideff_type
   | VtQed of vernac_qed_type
-  | VtProofStep of bool (* parallelize *)
+  | VtProofStep of proof_step
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * report_with
   | VtStm of vernac_control * vernac_part_of_script
@@ -476,6 +476,11 @@ and vernac_control =
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and proof_step = { (* TODO: inline with OCaml 4.03 *)
+  parallel : bool;
+  proof_block_detection : proof_block_name option
+}
+and proof_block_name = string (* open type of delimiters *)
 type vernac_when =
   | VtNow
   | VtLater
diff --git a/lib/flags.ml b/lib/flags.ml
index 4983e4082..3093e52b0 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,6 +68,9 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
+type tac_error_filter = [ `None | `Only of string list | `All ]
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ])
+let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index e13655e4a..d77681553 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,9 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
+type tac_error_filter = [ `None | `Only of string list | `All ]
+val async_proofs_tac_error_resilience : tac_error_filter ref
+val async_proofs_cmd_error_resilience : bool ref
 
 val debug : bool ref
 val in_debugger : bool ref
diff --git a/lib/stateid.ml b/lib/stateid.ml
index c17df2b32..500581a39 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -29,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
 let equal = Int.equal
 let compare = Int.compare
 
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
 
 type ('a,'b) request = {
   exn_info : t * t;
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 516ad891f..cd8fddf0c 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -11,7 +11,8 @@ type t
 val equal : t -> t -> bool
 val compare : t -> t -> int
 
-module Set : Set.S with type elt = t
+module Self : Map.OrderedType with type t = t
+module Set : Set.S with type elt = t and type t = Set.Make(Self).t
 
 val initial : t
 val dummy : t
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 5d3c149ab..57fad8511 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -872,7 +872,7 @@ END;;
    mode. *)
 VERNAC COMMAND EXTEND GrabEvars
 [ "Grab" "Existential" "Variables" ]
-  => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ]
+  => [ Vernac_classifier.classify_as_proofstep ]
   -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
 END
 
@@ -903,7 +903,7 @@ END
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
 [ "Unshelve" ]
-  => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ]
+  => [ Vernac_classifier.classify_as_proofstep ]
   -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p) ]
 END
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 3579fc10f..7c161e5cd 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -366,7 +366,8 @@ VERNAC tactic_mode EXTEND VernacSolve
     vernac_solve g n t def
   ]
 | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
-    [ VtProofStep true, VtLater ] -> [
+    [ VtProofStep{ parallel = true; proof_block_detection = Some "par" },
+      VtLater ] -> [
     vernac_solve SelectAll n t def
   ]
 END
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 0feba6365..73d3d1bab 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -100,7 +100,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
 
 let classify_proof_instr = function
   | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
-  | _ -> VtProofStep false, VtLater
+  | _ -> Vernac_classifier.classify_as_proofstep
 
 (* We use the VERNAC EXTEND facility with a custom non-terminal
     to populate [proof_mode] with a new toplevel interpreter.
diff --git a/stm/dag.ml b/stm/dag.ml
index 0c7f9f34b..99e7c9264 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 6b4442df0..e783cd8ee 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/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
new file mode 100644
index 000000000..ce12185cb
--- /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 { stop = entry_point.id; 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 { stop = entry_point.id; 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 { stop = entry_point.id; 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 { stop = entry_point.id; 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 000000000..a55032a47
--- /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/stm.ml b/stm/stm.ml
index e2acb1029..75d2e070a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -76,8 +76,14 @@ 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 ()
 
@@ -114,17 +120,31 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
   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 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
+      | Some (loc, ast) -> indentation, strlen, loc, ast
     with e when Errors.noncritical e ->
       let (e, info) = Errors.push e in
       let loc = Option.default Loc.ghost (Loc.get_loc info) in
@@ -140,7 +160,7 @@ 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
@@ -150,22 +170,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 *)
+  ctac : bool; (* is a tactic *)
   ceff : bool; (* is a side-effecting command in the middle of a proof *)
-  cast : ast;
+  cast : aast;
   cids : Id.t list;
-  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
-type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+  cblock : proof_block_name option;
+  cqueue : [ `MainQueue
+           | `TacQueue of 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
@@ -177,40 +202,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;
                        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 = {
+  start : Stateid.t;
+  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 (* {{{ *)
 
@@ -274,7 +328,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
 
@@ -288,30 +342,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 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 -> 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 : replay:ast option -> unit
+  val propagate_sideff : replay:aast option -> unit
 
   val gc : unit -> unit
 
@@ -327,7 +383,6 @@ end = struct (* {{{ *)
   include Vcs_
   exception Expired = Vcs_aux.Expired
 
-  module StateidSet = Set.Make(Stateid)
   open Printf
 
   let print_dag vcs () =
@@ -345,11 +400,11 @@ end = struct (* {{{ *)
       | 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 =
@@ -369,8 +424,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 -> ""
@@ -383,39 +436,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 =
@@ -452,13 +537,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 ())
 
@@ -508,9 +592,19 @@ end = struct (* {{{ *)
     let l = nodes_in_slice ~start ~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 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 start in
     let v = copy_info v start in
     let v = List.fold_right (fun (id,tr) v ->
@@ -518,28 +612,52 @@ end = struct (* {{{ *)
       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 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
+      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 stop in
     (* We put in the new dag the first state (since Qed shall run on it,
      * see check_task_aux) *)
-    copy_info_w_state v start
+    let v = copy_info_w_state v start in
+    copy_proof_blockes v
 
   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)
+  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 ~start:lemma =
+    if not (topo_invariant l) then anomaly (str "overlapping boxes");
+    vcs := create_property !vcs l (ProofTask { qed; lemma })
+  let create_proof_block ({ start; stop} as decl) name =
+    let l = nodes_in_slice ~start ~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 }
@@ -596,7 +714,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
 
 
@@ -616,6 +737,7 @@ 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
@@ -661,51 +783,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
@@ -714,7 +845,7 @@ 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) =
@@ -753,20 +884,22 @@ end = struct (* {{{ *)
       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 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 (* }}} *)
 
@@ -842,7 +975,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
 
@@ -941,6 +1074,75 @@ let _ = Errors.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
+    Errors.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 &&
+     (if Flags.async_proofs_is_master () then
+      !Flags.async_proofs_mode != Flags.APoff else true)
+  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 ({ start; stop } as decl) ->
+          VCS.create_proof_block decl name
+      end
+    with Not_found ->
+      Errors.errorlabstrm "STM"
+        (str "Unknown proof block delimiter " ++ str name)
+
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
 
@@ -1117,7 +1319,7 @@ 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;
@@ -1133,7 +1335,7 @@ end = struct (* {{{ *)
         let e_msg = iprint (e, info) 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 my_states in
+        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 =
@@ -1151,12 +1353,12 @@ 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
@@ -1258,7 +1460,7 @@ 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
@@ -1411,7 +1613,7 @@ and TacTask : sig
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : int * ast;
+    t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1428,7 +1630,7 @@ end = struct (* {{{ *)
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : int * ast;
+    t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1437,7 +1639,7 @@ end = struct (* {{{ *)
     r_state    : Stateid.t;
     r_state_fb : Stateid.t;
     r_document : VCS.vcs option;
-    r_ast      : int * ast;
+    r_ast      : int * aast;
     r_goal     : Goal.goal;
     r_name     : string }
 
@@ -1467,8 +1669,7 @@ end = struct (* {{{ *)
     match resp with
     | RespBuiltSubProof o -> t_assign (`Val o); `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 ((),[])
@@ -1496,7 +1697,7 @@ end = struct (* {{{ *)
          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 "^
+         Errors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
         let (i, ast) = r_ast in
@@ -1504,12 +1705,12 @@ end = struct (* {{{ *)
         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 -> Errors.errorlabstrm "STM" (str "no progress")
         | 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")
+            else Errors.errorlabstrm "STM" (str"The solution is not ground")
        end) ()
      in
        RespBuiltSubProof (t,uc)
@@ -1523,13 +1724,15 @@ end (* }}} *)
 and Partac : sig
 
   val vernac_interp :
-    cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit
+    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 vernac_interp cancel nworkers safe_id id
+    { indentation; verbose; loc; expr = e; strlen }
+  =
     let e, time, fail =
       let rec find time fail = function
         | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
@@ -1546,7 +1749,7 @@ end = struct (* {{{ *)
           Future.create_delegate
             ~name:(Printf.sprintf "subgoal %d" i)
             (State.exn_on id ~valid:safe_id) in
-        let t_ast = (i, { verbose; loc; expr = e }) 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;
@@ -1580,16 +1783,16 @@ 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"
@@ -1635,7 +1838,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 (* {{{ *)
 
@@ -1724,7 +1927,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
@@ -1760,7 +1963,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
 
@@ -1790,6 +1993,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 ({ stop } as decl, name) when Stateid.equal 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 ->
+          Errors.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 Errors.noncritical e ->
+        let ie = Errors.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 Errors.noncritical e -> () in
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
@@ -1808,9 +2076,9 @@ let known_state ?(redefine_qed=false) ~cache id =
   and reach ?(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 (fun () -> "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
@@ -1820,29 +2088,38 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
             reach view.next), cache, true
-      | `Cmd { cast = x; cqueue = `TacQueue 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 = `TacQueue cancel; cblock } -> (fun () ->
+            resilient_tactic id cblock (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))
           ), 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 ()), (if eff then `Yes else 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;
@@ -1859,7 +2136,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                 let drop_pt = keep == VtKeepAsAxiom in
                 let 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 ~start;
                 begin match brinfo, qed.fproof with
                 | { VCS.kind = `Edit _ }, None -> assert false
                 | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
@@ -2112,10 +2389,11 @@ let snapshot_vio ldir long_f_dot_v =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
+let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+  ({ verbose; loc; expr } as x) c
+ =
   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 (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
   let vcs = VCS.backup () in
   try
@@ -2170,7 +2448,7 @@ 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 }
+            {x with verbose = true }
            with e when Errors.noncritical e ->
              let e = Errors.push e in
              iraise (State.exn_on report_id e)); `Ok
@@ -2189,8 +2467,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
                     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")
@@ -2213,8 +2490,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 } -> ()
@@ -2229,11 +2505,14 @@ 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 = if parallel then `TacQueue (ref false) else `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
@@ -2250,8 +2529,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           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=in_proof;cast=x;cids=l;cqueue=`MainQueue });
+          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
@@ -2286,8 +2564,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
               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=in_proof;cast=x;cids=[];cqueue=`MainQueue });
+              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 ();
@@ -2299,11 +2576,11 @@ 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;
@@ -2324,19 +2601,30 @@ let get_ast id =
 
 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
+  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
 
@@ -2351,15 +2639,15 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) 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
     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 =
@@ -2384,7 +2672,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
@@ -2399,13 +2687,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 ();
@@ -2419,14 +2707,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
@@ -2441,14 +2729,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
@@ -2491,9 +2779,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 &&
diff --git a/stm/stm.mli b/stm/stm.mli
index 6ffe0beb4..37ec1f0a1 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -20,7 +20,9 @@ open Loc
    The sentence [s] is parsed in the state [ontop].
    If [newtip] is provided, then the returned state id is guaranteed to be
    [newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) ->
+val add :
+  ontop:Stateid.t -> ?newtip:Stateid.t ->
+  ?check:(vernac_expr located -> unit) ->
   bool -> edit_id -> string ->
     Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
@@ -96,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 = {
+  start : Stateid.t;
+  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
@@ -122,7 +200,8 @@ 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 ****************************** **)
 
diff --git a/stm/stm.mllib b/stm/stm.mllib
index bd792b01f..939ee187a 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -8,4 +8,5 @@ Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
 Stm
+ProofBlockDelimiter
 Vio_checking
diff --git a/stm/vcs.ml b/stm/vcs.ml
index 38c029901..c483ea4a9 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -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 8f22fee84..46b40f8a4 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 b1df3c9ca..a602d6b8a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,8 +21,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 " ^ if parallel then "par " else "" ^ 
+        Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
   | VtQuery (b,(id,route)) ->
       "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
@@ -93,7 +94,9 @@ let rec classify_vernac e =
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
           | VtStm _ | VtProofMode _ ), _ as x -> x
-        | VtQed _, _ -> VtProofStep false, VtNow
+        | VtQed _, _ ->
+            VtProofStep { parallel = false; proof_block_detection = None },
+            VtNow
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
@@ -105,12 +108,19 @@ let rec classify_vernac e =
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
     | VernacProof _ 
-    | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
-    | VernacSubproof _ | VernacEndSubproof
+    | VernacSubproof _
     | VernacCheckGuard
     | VernacUnfocused
-    | VernacSolveExistential _ -> VtProofStep false, VtLater
+    | VernacSolveExistential _ ->
+        VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+    | VernacBullet _ ->
+        VtProofStep { parallel = false; proof_block_detection = Some "bullet" },
+        VtLater
+    | VernacEndSubproof -> 
+        VtProofStep { parallel = false;
+                      proof_block_detection = Some "curly" },
+        VtLater
     (* Options changing parser *)
     | VernacUnsetOption (["Default";"Proof";"Using"])
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
@@ -219,4 +229,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 = false; proof_block_detection = None}, VtLater
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
new file mode 100644
index 000000000..31e349376
--- /dev/null
+++ b/test-suite/interactive/proof_block.v
@@ -0,0 +1,66 @@
+Goal False /\ True.
+Proof.
+split.
+  idtac.
+  idtac.
+  exact I.
+idtac.
+idtac.
+exact I.
+Qed.
+
+Lemma baz :  (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split. { eexists. split. par: trivial. }
+trivial.
+Qed.
+
+Lemma baz1 :  (True /\ False) /\ True.
+Proof.
+split. { split. par: trivial. }
+trivial.
+Qed.
+
+Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  { idtac.
+    unshelve eexists.
+    { apply 3. }
+    { split.
+      { idtac. trivialx. }
+      { reflexivity. } } }
+  trivial.
+Qed.
+
+Lemma foo1 : False /\ True.
+Proof.
+split.
+  { exact I. }
+  { exact I. }
+Qed.
+
+Definition banana := true + 4. 
+
+Check banana.
+
+Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  - idtac.
+    unshelve eexists.
+    + apply 3.
+    + split.
+      * idtacx. trivial. 
+      * reflexivity.
+  - trivial.
+Qed.
+
+Lemma baz2 :  ((1=0 /\ False) /\ True) /\ False.
+Proof.
+split. split. split.
+ - solve [ auto ].
+ - solve [ trivial ].
+ - solve [ trivial ].
+ - exact 6.
+Qed.
\ No newline at end of file
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index aab20650a..ceaaa112e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -379,6 +379,11 @@ let get_host_port opt s =
      prerr_endline ("Error: host:port or stdfds expected after option "^opt);
      exit 1
 
+let get_error_resilience opt = function
+  | "on" | "all" | "yes" -> `All
+  | "off" | "no" -> `None
+  | s -> `Only (String.split ',' s)
+
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
 let vio_tasks = ref []
@@ -492,6 +497,10 @@ let parse_args arglist =
         Flags.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
+    |"-async-proofs-tactic-error-resilience" ->
+        Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ())
+    |"-async-proofs-command-error-resilience" ->
+        Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
     |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())