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 | |
| 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')
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_1.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_1.v | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_2.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_2.v | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_3.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_3.v | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_4.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_ltac_4.v | 3 |
8 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_ltac_1.out b/test-suite/output/ErrorLocation_ltac_1.out new file mode 100644 index 0000000000..a9014c4b46 --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_1.out @@ -0,0 +1,3 @@ +File "stdin", line 2, characters 7-11: +Error: Tactic failure: Cannot solve this goal. + diff --git a/test-suite/output/ErrorLocation_ltac_1.v b/test-suite/output/ErrorLocation_ltac_1.v new file mode 100644 index 0000000000..368a4592f2 --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_1.v @@ -0,0 +1,3 @@ +Goal False. +idtac; easy. +Abort. diff --git a/test-suite/output/ErrorLocation_ltac_2.out b/test-suite/output/ErrorLocation_ltac_2.out new file mode 100644 index 0000000000..d38727ffa4 --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 7-8: +Error: Tactic failure. + diff --git a/test-suite/output/ErrorLocation_ltac_2.v b/test-suite/output/ErrorLocation_ltac_2.v new file mode 100644 index 0000000000..c3a9bd626a --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_2.v @@ -0,0 +1,4 @@ +Ltac f := fail. +Goal False. +idtac; f. +Abort. diff --git a/test-suite/output/ErrorLocation_ltac_3.out b/test-suite/output/ErrorLocation_ltac_3.out new file mode 100644 index 0000000000..409b72bba8 --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_3.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 7-10: +Error: Not a negated primitive equality. + diff --git a/test-suite/output/ErrorLocation_ltac_3.v b/test-suite/output/ErrorLocation_ltac_3.v new file mode 100644 index 0000000000..43ce1fc6e2 --- /dev/null +++ b/test-suite/output/ErrorLocation_ltac_3.v @@ -0,0 +1,4 @@ +Ltac inj := injection. +Goal False. +idtac; inj. +Abort. 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. + 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. |