diff options
| -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. |