diff options
| author | coqbot-app[bot] | 2020-09-25 15:06:01 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-25 15:06:01 +0000 |
| commit | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (patch) | |
| tree | 3ba7d6864516fe66ec17904d78cf1905c251d960 /test-suite | |
| parent | 39fe24769d18c21379f1123754fd606cdf8cd4c8 (diff) | |
| parent | fc0aa1e70cb1891ef3f62566af4e551d06bfb613 (diff) | |
Merge PR #12999: More improvements in locating tactic errors
Reviewed-by: ppedrot
Reviewed-by: ejgallego
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. |