14 files changed, 100 insertions, 19 deletions
diff --git a/test-suite/bugs/closed/bug_12414.v b/test-suite/bugs/closed/bug_12414.v
new file mode 100644
index 0000000000..50b4b86eff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12414.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Inductive list {T} : Type := | cons (t : T) : list -> list. (* who needs nil anyway? *)
+Arguments list : clear implicits.
+
+Fixpoint map {A B} (f: A -> B) (l : list A) : list B :=
+  let '(cons t l) := l in cons (f t) (map f l).
+About map@{_ _}.
+(* Two universes, as expected. *)
+
+Definition map_Set@{} {A B : Set} := @map A B.
+
+Definition map_Prop@{} {A B : Prop} := @map A B.
diff --git a/test-suite/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v
new file mode 100644
index 0000000000..9fdcb94e0c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12623.v
@@ -0,0 +1,18 @@
+Set Universe Polymorphism.
+
+Axiom M : Type -> Prop.
+Axiom raise : forall {T}, M T.
+
+Inductive goal : Type :=
+| AHyp : forall {A : Type}, goal.
+
+Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False).
+
+Class Seq (C : Type) :=
+  seq : C -> gtactic.
+Arguments seq {C _} _.
+
+Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise.
+
+Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise).
+Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise).
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v
index 0c236e12ad..00b9e9bd9d 100644
--- a/test-suite/bugs/closed/bug_5197.v
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {|
   rel := fun _ A => (forall ω : Ω, A ω) -> Type;
                           |}.
 Set Printing Universes.
-Fail Definition Typeᵇ : El Typeᶠ :=
+Definition Typeᵇ : El Typeᶠ :=
   mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
 
-Definition Typeᵇ : El Typeᶠ :=
-  mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+(* Definition Typeᵇ : El Typeᶠ := *)
+(*   mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *)
 
 (** Bidirectional typechecking helps here *)
 Require Import Program.Tactics.
diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake
new file mode 100644
index 0000000000..594ebced23
--- /dev/null
+++ b/test-suite/ide/proof-diffs.fake
@@ -0,0 +1,10 @@
+ADD { Goal True /\ False /\ True = False. }
+ADD { split. }
+GOALS
+ADD here { split. }
+GOALS
+PDIFF here
+ADD there { auto. }
+GOALS
+PDIFF there
+ADD { Admitted. }
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index abada44da7..bd22d45059 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -231,16 +231,13 @@ fun l : list nat => match l with
      : list nat -> list nat
 
 Arguments foo _%list_scope
-Notation
-"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
-(default interpretation)
-"'exists' ! x .. y , p" := ex
-                             (unique
-                                (fun x => .. (ex (unique (fun y => p))) ..))
-: type_scope (default interpretation)
-Notation
-"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
-(default interpretation)
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+  : type_scope (default interpretation)
+Notation "'exists' ! x .. y , p" :=
+  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope
+  (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
+  (default interpretation)
 1 subgoal
   
   ============================
diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out
index fca6dde704..54c4f98422 100644
--- a/test-suite/output/bug_12908.out
+++ b/test-suite/output/bug_12908.out
@@ -1,2 +1,7 @@
 forall m n : nat, m * n = (2 * m * n)%nat
      : Prop
+File "stdin", line 11, characters 0-31:
+Warning: Notation "_ * _" was already used in scope nat_scope.
+[notation-overridden,parsing]
+forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n
+     : Prop
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 558c9f9f6a..6f7be22fa0 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -1,6 +1,13 @@
 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.
+
+Module B.
+(* Test that an overriden scoped notation is deactivated *)
+Infix "*" := mult' : nat_scope.
+Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
+End B.
diff --git a/test-suite/output/bug_13112.out b/test-suite/output/bug_13112.out
new file mode 100644
index 0000000000..a8a98d6b68
--- /dev/null
+++ b/test-suite/output/bug_13112.out
@@ -0,0 +1,4 @@
+0 + 0
+     : nat
+HI
+     : nat
diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v
new file mode 100644
index 0000000000..9fee5e09d8
--- /dev/null
+++ b/test-suite/output/bug_13112.v
@@ -0,0 +1,5 @@
+Reserved Notation "'HI'".
+Notation "'HI'" := (O + O) (only parsing).
+Check HI. (* 0 + 0 : nat *)
+Notation "'HI'" := (O + O) (only printing).
+Check HI. (* 0 + 0 : nat *)
diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out
index ed4892b389..f035d0252a 100644
--- a/test-suite/output/bug_9180.out
+++ b/test-suite/output/bug_9180.out
@@ -1,4 +1,3 @@
-Notation
-"n .+1" := S n : nat_scope (default interpretation)
+Notation "n .+1" := (S n) : nat_scope (default interpretation)
 forall x : nat, x.+1 = x.+1
      : Prop
diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out
index e69de29bb2..45d9e4cad1 100644
--- a/test-suite/output/bug_9682.out
+++ b/test-suite/output/bug_9682.out
@@ -0,0 +1,9 @@
+mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x
+return M (x = x) with
+| 1
+end
+     : unit
+#
+     : True
+##
+     : True
diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v
index 3630142126..fa30d323ef 100644
--- a/test-suite/output/bug_9682.v
+++ b/test-suite/output/bug_9682.v
@@ -16,3 +16,13 @@ Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
     (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"
      ).
+(* Check use of "mmatch" *)
+Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end).
+
+(* 2nd example *)
+Notation "#" := I (at level 0, only parsing).
+Notation "#" := I (at level 0, only printing).
+Check #.
+Notation "##" := I (at level 0, only printing).
+Notation "##" := I (at level 0, only parsing).
+Check ##.
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 473db2d312..93d9d6cf7b 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,3 +1,2 @@
-Notation
-"b1 && b2" := if b1 then b2 else false (default interpretation)
-"x && y" := andb x y : bool_scope
+Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
+Notation "x && y" := (andb x y) : bool_scope
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9ab8ace39e..0796b507a1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -457,5 +457,10 @@ Module ObligationRegression.
   (** Test for a regression encountered when fixing obligations for
       stronger restriction of universe context. *)
   Require Import CMorphisms.
-  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _ _}.
+  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _}.
 End ObligationRegression.
+
+Axiom poly@{i} : forall(A : Type@{i}) (a : A), unit.
+
+Definition nonpoly := @poly True Logic.I.
+Definition check := nonpoly@{}.