diff options
| author | Hugo Herbelin | 2020-05-06 17:15:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-10 00:09:49 +0200 |
| commit | 403fe03748254d01618c05a4edd722bd56e957b9 (patch) | |
| tree | 79f9a1c516a65f9e8946c52aa104702c8d4dedec | |
| parent | 01e465952e79f4e7fdef3417c6f1883ca2c5e328 (diff) | |
Adding tests for error location
| -rw-r--r-- | test-suite/output/ErrorLocation_12152_1.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12152_1.v | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12152_2.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12152_2.v | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12255.out | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12255.v | 4 |
6 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_12152_1.out b/test-suite/output/ErrorLocation_12152_1.out new file mode 100644 index 0000000000..b7b600d53d --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-7: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v new file mode 100644 index 0000000000..e63ab1cd48 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intro H; auto. diff --git a/test-suite/output/ErrorLocation_12152_2.out b/test-suite/output/ErrorLocation_12152_2.out new file mode 100644 index 0000000000..bdfd0a050f --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-8: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v new file mode 100644 index 0000000000..5df6bec939 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intros H; auto. diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out new file mode 100644 index 0000000000..ed5e183427 --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 0-16: +Error: Ltac variable x is bound to i > 0 which cannot be coerced to +an evaluable reference. + diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v new file mode 100644 index 0000000000..347424b2fc --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.v @@ -0,0 +1,4 @@ +Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. +Definition i := O. +Goal False. +can_unfold (i>0). |