From f4adca746b5434997d434df5dcc6bf010a196f23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 13:41:18 +0200
Subject: Fixes #13241 (nested Ltac functions were wrongly reporting error on
 the inner calls).

This continues #12223, #12773, #12992, #12774, #12999.
---
 test-suite/output/ErrorLocation_13241_1.out | 3 +++
 test-suite/output/ErrorLocation_13241_1.v   | 4 ++++
 test-suite/output/ErrorLocation_13241_2.out | 3 +++
 test-suite/output/ErrorLocation_13241_2.v   | 4 ++++
 4 files changed, 14 insertions(+)
 create mode 100644 test-suite/output/ErrorLocation_13241_1.out
 create mode 100644 test-suite/output/ErrorLocation_13241_1.v
 create mode 100644 test-suite/output/ErrorLocation_13241_2.out
 create mode 100644 test-suite/output/ErrorLocation_13241_2.v

(limited to 'test-suite')

diff --git a/test-suite/output/ErrorLocation_13241_1.out b/test-suite/output/ErrorLocation_13241_1.out
new file mode 100644
index 0000000000..d899dd5d46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_1.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v
new file mode 100644
index 0000000000..ff92085133
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_1.v
@@ -0,0 +1,4 @@
+Ltac a := intro.
+Ltac b := a.
+Goal True.
+b.
diff --git a/test-suite/output/ErrorLocation_13241_2.out b/test-suite/output/ErrorLocation_13241_2.out
new file mode 100644
index 0000000000..d899dd5d46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_2.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v
new file mode 100644
index 0000000000..280d4a3506
--- /dev/null
+++ b/test-suite/output/ErrorLocation_13241_2.v
@@ -0,0 +1,4 @@
+Ltac a _ := intro.
+Ltac b := a ().
+Goal True.
+b.
-- 
cgit v1.2.3