diff options
| -rw-r--r-- | test-suite/output/ErrorLocation_12152_1.v | 1 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12152_2.v | 1 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12255.v | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v index e63ab1cd48..709ac305e4 100644 --- a/test-suite/output/ErrorLocation_12152_1.v +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -1,3 +1,4 @@ (* Reported in #12152 *) Goal True. intro H; auto. +Abort. diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v index 5df6bec939..29e4c910d8 100644 --- a/test-suite/output/ErrorLocation_12152_2.v +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -1,3 +1,4 @@ (* Reported in #12152 *) Goal True. intros H; auto. +Abort. diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v index 347424b2fc..59c0e1dfc5 100644 --- a/test-suite/output/ErrorLocation_12255.v +++ b/test-suite/output/ErrorLocation_12255.v @@ -2,3 +2,4 @@ Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. Definition i := O. Goal False. can_unfold (i>0). +Abort. |