11 files changed, 52 insertions, 6 deletions
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
index 961b170a0d..ba0bcb1b3c 100644
--- a/test-suite/misc/quotation_token/src/quotation.mlg
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -2,9 +2,9 @@
 open Pcoq.Constr
 }
 GRAMMAR EXTEND Gram
-  GLOBAL: operconstr;
+  GLOBAL: term;
 
-  operconstr: LEVEL "0"
+  term: LEVEL "0"
     [ [ s = QUOTATION "foobar:" ->
         {
           CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index da2fc90fc3..01564e7f25 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -178,3 +178,6 @@ match N with
 | _ => Node
 end
      : Tree -> Tree
+File "stdin", line 253, characters 4-5:
+Warning: Unused variable B catches more than one case.
+[unused-pattern-matching-variable,pattern-matching]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 262ec2b677..2d8a8b359c 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -242,3 +242,15 @@ end.
 Print stray.
 
 End Bug11231.
+
+Module Wish12762.
+
+Inductive foo := a | b | c.
+
+Definition bar (f : foo) :=
+  match f with
+  | a => 0
+  | B => 1
+  end.
+
+End Wish12762.
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/Notations4.out b/test-suite/output/Notations4.out
index a42518822f..fa0c20bf73 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -8,7 +8,7 @@ Entry custom:myconstr is
 | "4" RIGHTA
   [ SELF; "*"; NEXT ]
 | "3" RIGHTA
-  [ "<"; operconstr LEVEL "10"; ">" ] ]
+  [ "<"; term LEVEL "10"; ">" ] ]
 
 [< b > + < b > * < 2 >]
      : nat
@@ -77,7 +77,7 @@ The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 Entry custom:expr is
 [ "201" RIGHTA
-  [ "{"; operconstr LEVEL "200"; "}" ] ]
+  [ "{"; term LEVEL "200"; "}" ] ]
 
 fun x : nat => [ x ]
      : nat -> nat
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
new file mode 100644
index 0000000000..a17d05200d
--- /dev/null
+++ b/test-suite/output/bug_13238.out
@@ -0,0 +1,4 @@
+Ltac t1 x := replace (x x) with (x x)
+Ltac t2 x := case : x 
+Ltac t3 := by move ->
+Ltac t4 := congr True 
diff --git a/test-suite/output/bug_13238.v b/test-suite/output/bug_13238.v
new file mode 100644
index 0000000000..9b8063bf13
--- /dev/null
+++ b/test-suite/output/bug_13238.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Ltac t1 x := replace (x x) with (x x).
+Print t1.
+
+Ltac t2 x := case: x.
+Print t2.
+
+Ltac t3 := by move->.
+Print t3.
+
+Ltac t4 := congr True.
+Print t4.