From 05eb5d91989c0d0c470a1b35af52c84a60853f89 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 29 Jul 2020 17:59:35 +0200
Subject: Remaining bugs in PR#12223 which fixed location of tactic errors
 (issue #12152).

The update of a loc needs sometimes to override (when calling an Ltac
function), and otherwise to keep the existing loc (assumed to be
fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests).

Moreover, when overriding, this was going to a tclOR backtracking
point which was setting the loc to a completely disjoint part of the
code having caused the error (see #12773). We replace the tclOR by a
tclORELSE.
---
 test-suite/output/ErrorLocation_12774_1.out       | 3 +++
 test-suite/output/ErrorLocation_12774_1.v         | 3 +++
 test-suite/output/ErrorLocation_12774_2.out       | 3 +++
 test-suite/output/ErrorLocation_12774_2.v         | 4 ++++
 test-suite/output/ErrorLocation_tac_in_term_1.out | 4 ++++
 test-suite/output/ErrorLocation_tac_in_term_1.v   | 3 +++
 test-suite/output/ErrorLocation_tac_in_term_2.out | 4 ++++
 test-suite/output/ErrorLocation_tac_in_term_2.v   | 5 +++++
 8 files changed, 29 insertions(+)
 create mode 100644 test-suite/output/ErrorLocation_12774_1.out
 create mode 100644 test-suite/output/ErrorLocation_12774_1.v
 create mode 100644 test-suite/output/ErrorLocation_12774_2.out
 create mode 100644 test-suite/output/ErrorLocation_12774_2.v
 create mode 100644 test-suite/output/ErrorLocation_tac_in_term_1.out
 create mode 100644 test-suite/output/ErrorLocation_tac_in_term_1.v
 create mode 100644 test-suite/output/ErrorLocation_tac_in_term_2.out
 create mode 100644 test-suite/output/ErrorLocation_tac_in_term_2.v

(limited to 'test-suite/output')

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.
-- 
cgit v1.2.3