7 files changed, 29 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/bug_13276.v b/test-suite/bugs/closed/bug_13276.v
new file mode 100644
index 0000000000..15ac7e7b36
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13276.v
@@ -0,0 +1,9 @@
+From Coq Require Import Floats.
+Open Scope float_scope.
+
+Lemma foo :
+  let n := opp 0 in sub n 0 = n.
+Proof.
+cbv.
+apply eq_refl.
+Qed.
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.
diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out
index 2bd7d67535..28bc580202 100644
--- a/test-suite/output/bug_13004.out
+++ b/test-suite/output/bug_13004.out
@@ -1,2 +1,2 @@
-Ltac bug_13004.t := ltac2:(print (of_string "hi"))
-Ltac bug_13004.u := ident:(H)
+Ltac t := ltac2:(print (of_string "hi"))
+Ltac u := ident:(H)
diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out
index bda21aa9e3..a17d05200d 100644
--- a/test-suite/output/bug_13238.out
+++ b/test-suite/output/bug_13238.out
@@ -1,4 +1,4 @@
-Ltac bug_13238.t1 x := replace (x x) with (x x)
-Ltac bug_13238.t2 x := case : x 
-Ltac bug_13238.t3 := by move ->
-Ltac bug_13238.t4 := congr True 
+Ltac t1 x := replace (x x) with (x x)
+Ltac t2 x := case : x 
+Ltac t3 := by move ->
+Ltac t4 := congr True