13 files changed, 129 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/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.
diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v
new file mode 100644
index 0000000000..120e62b145
--- /dev/null
+++ b/test-suite/success/definition_using.v
@@ -0,0 +1,68 @@
+Require Import Program.
+Axiom bogus : Type.
+
+Section A.
+Variable x : bogus.
+
+#[using="All"]
+Definition c1 : bool := true.
+
+#[using="All"]
+Fixpoint c2 n : bool :=
+  match n with
+  | O => true
+  | S p => c3 p
+  end
+with c3 n : bool :=
+  match n with
+  | O => true
+  | S p => c2 p
+end.
+
+#[using="All"]
+Definition c4 : bool. Proof. exact true. Qed.
+
+#[using="All"]
+Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed.
+
+#[using="All", program]
+Definition c6 : bool. Proof. exact true. Qed.
+
+#[using="All", program]
+Fixpoint c7 (n : nat) {struct n} : bool :=
+  match n with
+  | O => true
+  | S p => c7 p
+  end.
+
+End A.
+
+Check c1 : bogus -> bool.
+Check c2 : bogus -> nat -> bool.
+Check c3 : bogus -> nat -> bool.
+Check c4 : bogus -> bool.
+Check c5 : bogus -> nat -> bool.
+Check c6 : bogus -> bool.
+Check c7 : bogus -> nat -> bool.
+
+Section B.
+
+Variable a : bogus.
+Variable h : c1 a = true.
+
+#[using="a*"]
+Definition c8 : bogus := a.
+
+Collection ccc := a h.
+
+#[using="ccc"]
+Definition c9 : bogus := a.
+
+#[using="ccc - h"]
+Definition c10 : bogus := a.
+
+End B.
+
+Check c8 : forall a, c1 a = true -> bogus.
+Check c9 : forall a, c1 a = true -> bogus.
+Check c10: bogus -> bogus.