From 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 11:11:30 +0200
Subject: STM: proof block detection/error resilience API

This commit introduces the concept of proof blocks that are
resilient to errors.  They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.

The detection and error recovery of ErrorBound boxes is defined outside
the STM.  One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
---
 ltac/extratactics.ml4 | 4 ++--
 ltac/g_ltac.ml4       | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 5d3c149ab9..57fad85113 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 3579fc10f6..c8287a2c8d 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 = None },
+      VtLater ] -> [
     vernac_solve SelectAll n t def
   ]
 END
-- 
cgit v1.2.3


From 8baf120d5cf5045d188f7d926162643a6e7ebcd0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 13:46:43 +0200
Subject: STM: proof block detection for par:

"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
---
 ltac/g_ltac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index c8287a2c8d..7c161e5cdc 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -366,7 +366,7 @@ VERNAC tactic_mode EXTEND VernacSolve
     vernac_solve g n t def
   ]
 | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
-    [ VtProofStep{ parallel = true; proof_block_detection = None },
+    [ VtProofStep{ parallel = true; proof_block_detection = Some "par" },
       VtLater ] -> [
     vernac_solve SelectAll n t def
   ]
-- 
cgit v1.2.3