diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-23 11:11:30 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:48:44 -0400 |
| commit | 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (patch) | |
| tree | c803222d842bd96f3a25852633288e3aab14f45f /ltac | |
| parent | 07115d044cb97bc6c0a7323783d4d53e083d3e89 (diff) | |
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.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | ltac/g_ltac.ml4 | 3 |
2 files changed, 4 insertions, 3 deletions
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..c8287a2c8 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 |