diff options
| author | Jason Gross | 2019-10-25 15:28:37 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-10-29 12:32:57 -0400 |
| commit | c59815c860a11948359e96ecc51d566bb5e5d8fb (patch) | |
| tree | bdd7e2d7dbcf38e6e2d27de71a3d94dc80f46347 /test-suite | |
| parent | e9dddcb2b5297f2e601a2e2d65a131ee5fde19e4 (diff) | |
`assert_succeeds`&`assert_fails`: multisuccess fix
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Tactics.out | 1 | ||||
| -rw-r--r-- | test-suite/output/Tactics.v | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 19c9fc4423..70427220ed 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -6,3 +6,4 @@ The command has indeed failed with message: H is already used. The command has indeed failed with message: H is already used. +a diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index fa12f09a46..96b6d652c9 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -22,3 +22,11 @@ intros H. Fail intros [H%myid ?]. Fail destruct 1 as [H%myid ?]. Abort. + + +(* Test that assert_succeeds only runs a tactic once *) +Ltac should_not_loop := idtac + should_not_loop. +Goal True. + assert_succeeds should_not_loop. + assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) +Abort. |