10 files changed, 89 insertions, 18 deletions
diff --git a/test-suite/bugs/closed/bug_12917.v b/test-suite/bugs/closed/bug_12917.v
new file mode 100644
index 0000000000..cd6b0766c6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12917.v
@@ -0,0 +1 @@
+Fail Derive Inversion bla with (le _ _).
diff --git a/test-suite/bugs/closed/bug_13059.v b/test-suite/bugs/closed/bug_13059.v
new file mode 100644
index 0000000000..2416e3ad13
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13059.v
@@ -0,0 +1,31 @@
+Set Uniform Inductive Parameters.
+Inductive test (X : Set) : Prop :=
+with test2 (X : Set) : X -> Prop :=
+ | C (x : X) : test2 x.
+
+Require Import List.
+Import ListNotations.
+
+Set Suggest Proof Using.
+Set Primitive Projections.
+
+
+Section Grammar.
+Variable A : Type.
+
+Record grammar : Type := Grammar {
+  gm_nonterm :> Type ;
+  gm_rules :> list (gm_nonterm * list (A + gm_nonterm)) ;
+}.
+
+Set Uniform Inductive Parameters.
+Inductive lang (gm : grammar) : gm -> list A -> Prop :=
+| lang_rule S ps ws : In (S, ps) gm -> lmatch ps ws -> lang S (concat ws)
+with lmatch (gm : grammar) : list (A + gm) -> list (list A) -> Prop :=
+| lmatch_nil : lmatch [] []
+| lmatch_consL ps ws a : lmatch ps ws -> lmatch (inl a :: ps) ([a] :: ws)
+| lmatch_consR ps ws S w :
+    lang S w -> lmatch ps ws -> lmatch (inr S :: ps) (w :: ws)
+.
+
+End Grammar.
diff --git a/test-suite/bugs/closed/bug_13109.v b/test-suite/bugs/closed/bug_13109.v
new file mode 100644
index 0000000000..76511a44c5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13109.v
@@ -0,0 +1,24 @@
+Require Import Coq.Program.Tactics.
+
+Set Universe Polymorphism.
+Obligation Tactic := idtac.
+
+Program Definition foo : Type := _.
+Program Definition bar : Type := _.
+Admit Obligations.
+(* Error: Anomaly "Uncaught exception AcyclicGraph.Make(Point).AlreadyDeclared."
+Please report at http://coq.inria.fr/bugs/.
+ *)
+Print foo.
+Print foo_obligation_1.
+Print bar.
+Print bar_obligation_1.
+
+Program Definition baz : Type := _.
+Admit Obligations of baz.
+Print baz.
+Print baz_obligation_1.
+
+Admit Obligations.
+
+Fail Admit Obligations of nobody.
diff --git a/test-suite/bugs/closed/bug_2928.v b/test-suite/bugs/closed/bug_2928.v
deleted file mode 100644
index 21e92ae20c..0000000000
--- a/test-suite/bugs/closed/bug_2928.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Class Equiv A := equiv: A -> A -> Prop.
-Infix "=" := equiv : type_scope.
-
-Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
-
-Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
-
-Class SemiLattice A op `{Equiv A} :=
-    { semilattice_sg :>> SemiGroup A op
-    ; redundant : Associative op
-    }.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index ce51acac95..a42518822f 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,6 +1,6 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
-Entry constr:myconstr is
+Entry custom:myconstr is
 [ "6" RIGHTA
   [  ]
 | "5" RIGHTA
@@ -8,7 +8,7 @@ Entry constr:myconstr is
 | "4" RIGHTA
   [ SELF; "*"; NEXT ]
 | "3" RIGHTA
-  [ "<"; constr:operconstr LEVEL "10"; ">" ] ]
+  [ "<"; operconstr LEVEL "10"; ">" ] ]
 
 [< b > + < b > * < 2 >]
      : nat
@@ -75,9 +75,9 @@ The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 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 constr:expr is
+Entry custom:expr is
 [ "201" RIGHTA
-  [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
+  [ "{"; operconstr LEVEL "200"; "}" ] ]
 
 fun x : nat => [ x ]
      : nat -> nat
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 163ed15606..d8d3f696b7 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -67,9 +67,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.33} in
-let ff := Type@{UnivBinders.35} in tt -> ff
-     : Type@{max(UnivBinders.32,UnivBinders.34)}
+let tt := Type@{UnivBinders.32} in
+let ff := Type@{UnivBinders.34} in tt -> ff
+     : Type@{max(UnivBinders.31,UnivBinders.33)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out
new file mode 100644
index 0000000000..fca6dde704
--- /dev/null
+++ b/test-suite/output/bug_12908.out
@@ -0,0 +1,2 @@
+forall m n : nat, m * n = (2 * m * n)%nat
+     : Prop
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
new file mode 100644
index 0000000000..558c9f9f6a
--- /dev/null
+++ b/test-suite/output/bug_12908.v
@@ -0,0 +1,6 @@
+Definition mult' m n := 2 * m * n.
+Module A.
+(* Test hiding of a scoped notation by a lonely notation *)
+Infix "*" := mult'.
+Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
+End A.
diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/bug_9682.out
diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v
new file mode 100644
index 0000000000..3630142126
--- /dev/null
+++ b/test-suite/output/bug_9682.v
@@ -0,0 +1,18 @@
+Declare Scope blafu.
+Delimit Scope blafu with B.
+Axiom DoesNotMatch : Type.
+Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit.
+
+Notation "|  p1  |  ..  |  pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu.
+Notation "'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" :=
+    (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
+      (at level 200, ls at level 91, only parsing).
+Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
+  (mmatch_do_not_write x in T as y return M p with_do_not_write ls)
+    (at level 200, ls at level 91, p at level 10, only parsing).
+(* This should not gives a warning *)
+Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
+  (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
+    (at level 200, ls at level 91, p at level 10, only printing,
+     format "'[  ' mmatch  '/' x ']'  '/' '[  ' in  '/' T ']'  '/' '[  ' as  '/' y ']'  '/' '[  ' return  M  p ']'  with  '//' '[' ls ']'  '//' end"
+     ).