diff options
| author | Théo Zimmermann | 2020-05-25 15:05:28 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-25 18:50:47 +0200 |
| commit | 488cd018153a13fd9136415751c57d48c7ac7d5c (patch) | |
| tree | 1b01ec95f390ab9f2a0284e77016709d8749a292 | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Fix output tests for location errors when running in async mode.
In this mode, an additional error was emitted, which made the test fail:
Error: There are pending proofs: Unnamed_thm.
| -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. |