diff options
| author | Pierre-Marie Pédrot | 2020-05-12 21:07:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 21:07:43 +0200 |
| commit | 942a198f7e70c5cf3e4bf39232da8b5b26c79d61 (patch) | |
| tree | 6cda67c289a53cdafebe9c4ebe189490dada8d2f /test-suite | |
| parent | 5784bb98aaa3e4eab4cd3e9871afb4b40d82f62c (diff) | |
| parent | cb14a7ebfbad02d954bc2ffa9c924c95f6dd5543 (diff) | |
Merge PR #12223: Locating error again in atomic tactics (fixes #12152)
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -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). |