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.out | |
| 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.out')
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_4.out | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_ltac_4.out b/test-suite/output/ErrorLocation_ltac_4.out new file mode 100644 index 0000000000..f9107cdc3f --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_4.out @@ -0,0 +1,3 @@ +File "stdin", line 2, characters 22-23: +Error: Tactic failure. + |