diff options
| author | Hugo Herbelin | 2020-09-09 12:58:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-16 08:08:18 +0200 |
| commit | fc0aa1e70cb1891ef3f62566af4e551d06bfb613 (patch) | |
| tree | bda03cc9cd546c2c7355f9f6ff893bd6612a9e51 /test-suite/output/ErrorLocation_ltac_4.v | |
| parent | d6b6e1d6ceadfe65ea398786361ff7737624deaf (diff) | |
More improvements in locating tactic errors.
We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.
Diffstat (limited to 'test-suite/output/ErrorLocation_ltac_4.v')
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_4.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_ltac_4.v b/test-suite/output/ErrorLocation_ltac_4.v new file mode 100644 index 0000000000..58c370c31b --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_4.v @@ -0,0 +1,3 @@ +Goal False. +let x := fail in x || x. +Abort. |