diff options
Diffstat (limited to 'test-suite/output')
| -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. |