diff options
| author | Pierre-Marie Pédrot | 2020-08-19 00:38:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-19 00:38:54 +0200 |
| commit | daed771ff18978dea536b277e00c0ca0149129ee (patch) | |
| tree | 98a50807d4a622c8b78ef247fe1dc391b6dbdba5 /test-suite | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
| parent | 05eb5d91989c0d0c470a1b35af52c84a60853f89 (diff) | |
Merge PR #12774: Fixing tactic loc updating in #12223
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_1.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_1.v | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_2.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_12774_2.v | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_tac_in_term_1.out | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_tac_in_term_1.v | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_tac_in_term_2.out | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_tac_in_term_2.v | 5 |
8 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/output/ErrorLocation_12774_1.out b/test-suite/output/ErrorLocation_12774_1.out new file mode 100644 index 0000000000..e27992ed59 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_1.out @@ -0,0 +1,3 @@ +File "stdin", line 2, characters 13-14: +Error: The term "0" has type "nat" while it is expected to have type "Type". + diff --git a/test-suite/output/ErrorLocation_12774_1.v b/test-suite/output/ErrorLocation_12774_1.v new file mode 100644 index 0000000000..8516d402d1 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_1.v @@ -0,0 +1,3 @@ +Goal Type. +simpl; exact 0. +Abort. diff --git a/test-suite/output/ErrorLocation_12774_2.out b/test-suite/output/ErrorLocation_12774_2.out new file mode 100644 index 0000000000..434275eca5 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 9-10: +Error: The term "0" has type "nat" while it is expected to have type "Type". + diff --git a/test-suite/output/ErrorLocation_12774_2.v b/test-suite/output/ErrorLocation_12774_2.v new file mode 100644 index 0000000000..e50e1caa0f --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_2.v @@ -0,0 +1,4 @@ +Ltac f := simpl. +Goal Type. +f; exact 0. +Abort. diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.out b/test-suite/output/ErrorLocation_tac_in_term_1.out new file mode 100644 index 0000000000..55ad5a36da --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_1.out @@ -0,0 +1,4 @@ +File "stdin", line 2, characters 21-25: +Error: +The term "true" has type "bool" while it is expected to have type "nat". + diff --git a/test-suite/output/ErrorLocation_tac_in_term_1.v b/test-suite/output/ErrorLocation_tac_in_term_1.v new file mode 100644 index 0000000000..ef0b5aa757 --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_1.v @@ -0,0 +1,3 @@ +Goal True. +apply ltac:(apply (S true)). +Abort. diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.out b/test-suite/output/ErrorLocation_tac_in_term_2.out new file mode 100644 index 0000000000..5bff5ede43 --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_2.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 12-20: +Error: +The term "true" has type "bool" while it is expected to have type "nat". + diff --git a/test-suite/output/ErrorLocation_tac_in_term_2.v b/test-suite/output/ErrorLocation_tac_in_term_2.v new file mode 100644 index 0000000000..e0fc2a9f4f --- /dev/null +++ b/test-suite/output/ErrorLocation_tac_in_term_2.v @@ -0,0 +1,5 @@ +Ltac f x y := apply (x y). + +Goal True. +apply ltac:(f S true). +Abort. |