diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9114.v | 5 | ||||
| -rw-r--r-- | test-suite/output/Tactics.out | 1 | ||||
| -rw-r--r-- | test-suite/output/Tactics.v | 8 |
3 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v new file mode 100644 index 0000000000..2cf91c1c2b --- /dev/null +++ b/test-suite/bugs/closed/bug_9114.v @@ -0,0 +1,5 @@ +Goal True. + assert_succeeds (exact I). + idtac. + (* Error: No such goal. *) +Abort. 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. |