diff options
| author | Théo Zimmermann | 2020-11-03 14:28:35 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-03 14:28:35 +0100 |
| commit | 2812f8323e46e22ccde1606c71d908059b732e44 (patch) | |
| tree | f1ac258e10505f1322caba0debfdf515415a728f | |
| parent | dfdecf24210ee287d554cf4296bd0ccfffe310d8 (diff) | |
Fix test-suite in async mode.
(By closing unfinished proofs.)
| -rw-r--r-- | test-suite/output/ErrorLocation_13241_1.v | 1 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_13241_2.v | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v index ff92085133..3102b13fb8 100644 --- a/test-suite/output/ErrorLocation_13241_1.v +++ b/test-suite/output/ErrorLocation_13241_1.v @@ -2,3 +2,4 @@ Ltac a := intro. Ltac b := a. Goal True. b. +Abort. diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v index 280d4a3506..b82f36ed6f 100644 --- a/test-suite/output/ErrorLocation_13241_2.v +++ b/test-suite/output/ErrorLocation_13241_2.v @@ -2,3 +2,4 @@ Ltac a _ := intro. Ltac b := a (). Goal True. b. +Abort. |