diff options
| author | Pierre-Marie Pédrot | 2020-08-21 17:04:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-21 17:04:02 +0200 |
| commit | f149d617b631d6fc64937d3882ed3db16fdf6c8f (patch) | |
| tree | 06da1441527b7aa154b18289bbf3b253ea307ca3 /test-suite | |
| parent | 85dad6f7b52c8b84a87e61eb45dbc1f28c8780ae (diff) | |
| parent | f10b2021cce7bca2d0234e9ab73be47cdc3bf6fc (diff) | |
Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_3.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_3.v | 4 | ||||
| -rw-r--r-- | test-suite/output/Error_msg_diffs.out | 2 |
3 files changed, 8 insertions, 1 deletions
diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out new file mode 100644 index 0000000000..dbd3dbd1e2 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v new file mode 100644 index 0000000000..c624402a81 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.v @@ -0,0 +1,4 @@ +Ltac f := auto; intro. +Goal False. +f. +Abort. diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out index 3e337e892d..2645524a70 100644 --- a/test-suite/output/Error_msg_diffs.out +++ b/test-suite/output/Error_msg_diffs.out @@ -1,4 +1,4 @@ -File "stdin", line 32, characters 0-12: +File "stdin", line 32, characters 0-11: [37;41;1mError:[0m In environment T : [33;1mType[0m |