diff options
| author | Emilio Jesus Gallego Arias | 2020-05-27 11:44:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-27 11:44:49 +0200 |
| commit | 35e175710795974a4a38c8a7d6da6a5ccaf8de74 (patch) | |
| tree | d2f765126a399e45b4e32a86a434b0b61dc456b5 | |
| parent | 1eb5f0504561224affd93717a9fca0e3162dcdd9 (diff) | |
| parent | 488cd018153a13fd9136415751c57d48c7ac7d5c (diff) | |
Merge PR #12408: Fix output tests for location errors when running in async mode.
Reviewed-by: JasonGross
Reviewed-by: ejgallego
| -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. |