aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-14 10:51:00 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-14 10:51:00 +0200
commitff67a511a358ada3daefea0839e18d474531e13d (patch)
treeb5dfb7b8d79394d1aabbe0d125d30e12a0fbf621 /ltac
parent19330a458b907b5e66a967adbfe572d92194913c (diff)
parent1334a657052a2385c3f3b01cc65c3ccae448fa96 (diff)
Merge remote-tracking branch 'origin/pr/173' into trunk
This is the "error resiliency" mode for STM
Diffstat (limited to 'ltac')
-rw-r--r--ltac/extratactics.ml44
-rw-r--r--ltac/g_ltac.ml43
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..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