19 files changed, 437 insertions, 42 deletions
diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v
new file mode 100644
index 0000000000..797146174d
--- /dev/null
+++ b/test-suite/bugs/closed/3125.v
@@ -0,0 +1,27 @@
+(* Not considering singleton template-polymorphic inductive types as
+   propositions for injection/inversion *)
+
+(* This is also #4560 and #6273 *)
+
+Inductive foo := foo_1.
+
+Goal forall (a b : foo), Some a = Some b -> a = b.
+Proof.
+  intros a b H.
+  inversion H.
+  reflexivity.
+Qed.
+
+(* Check that Prop is not concerned *)
+
+Inductive bar : Prop := bar_1.
+
+Goal
+  forall (a b : bar),
+    Some a = Some b ->
+    a = b.
+Proof.
+  intros a b H.
+  inversion H.
+  Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index da12b68689..5210b27032 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -65,6 +65,7 @@ Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A
 = B.
 Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
 Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V.
+Existing Instance is0trunc_V.
 Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.
 Axiom bisimulation_refl : forall (v : V), bisimulation v v.
 Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v.
diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
index a96a137001..c069b2d9dc 100644
--- a/test-suite/bugs/closed/4390.v
+++ b/test-suite/bugs/closed/4390.v
@@ -8,16 +8,16 @@ Universe i.
 End foo.
 End M.
 
-Check Type@{i}.
+Check Type@{M.i}.
 (* Succeeds *)
 
 Fail Check Type@{j}.
 (* Error: Undeclared universe: j *)
 
-Definition foo@{j} : Type@{i} := Type@{j}.
+Definition foo@{j} : Type@{M.i} := Type@{j}.
 (* ok *)
 End A.
-
+Import A. Import M.
 Set Universe Polymorphism.
 Fail Universes j.
 Monomorphic Universe j.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index b4c745375f..d02a5f120c 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C)
 
 Generalizable All Variables.
 Axiom fs : Funext.
+Existing Instance fs.
 
 Section bar.
 
diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out
new file mode 100644
index 0000000000..29d50775a9
--- /dev/null
+++ b/test-suite/output/Extraction_infix.out
@@ -0,0 +1,20 @@
+(** val test : foo **)
+
+let test =
+  (fun (b, p) -> bar) (True, False)
+(** val test : foo **)
+
+let test =
+  True@@?False
+(** val test : foo **)
+
+let test =
+  True#^^False
+(** val test : foo **)
+
+let test =
+  True@?:::False
+(** val test : foo **)
+
+let test =
+  True  @?:::  False
diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v
new file mode 100644
index 0000000000..fe5926a36a
--- /dev/null
+++ b/test-suite/output/Extraction_infix.v
@@ -0,0 +1,26 @@
+(* @herbelin's example for issue #6212 *)
+
+Require Import Extraction.
+Inductive I := C : bool -> bool -> I.
+Definition test := C true false.
+
+(* the parentheses around the function wrong signalled an infix operator *)
+
+Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ].
+Extraction test.
+
+(* some bonafide infix operators *)
+
+Extract Inductive I => "foo" [ "(@@?)" ].
+Extraction test.
+
+Extract Inductive I => "foo" [ "(#^^)" ].
+Extraction test.
+
+Extract Inductive I => "foo" [ "(@?:::)" ].
+Extraction test.
+
+(* allow whitespace around infix operator *)
+
+Extract Inductive I => "foo" [ "(  @?:::  )" ].
+Extraction test.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 7bcd7b041c..2f0ee765db 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -64,7 +64,7 @@ The command has indeed failed with message:
 Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
 Both ends of the recursive pattern are the same.
-SUM (nat * nat) nat
+(nat * nat + nat)%type
      : Set
 FST (0; 1)
      : Z
@@ -72,7 +72,7 @@ Nil
      : forall A : Type, list A
 NIL : list nat
      : list nat
-(false && I 3)%bool /\ I 6
+(false && I 3)%bool /\ (I 6)%bool
      : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index fe6c05c39e..413812ee19 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)).
 
 Section A.
 
-Notation "! A" := (forall _:nat, A) (at level 60).
+Notation "! A" := (forall _:nat, A) (at level 60) : type_scope.
 
 Check ! (0=0).
 Check forall n, n=0.
@@ -194,9 +194,9 @@ Open Scope nat_scope.
 
 Coercion is_true := fun b => b=true.
 Coercion of_nat n := match n with 0 => true | _ => false end.
-Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope.
 
-Check (false && I 3)%bool /\ I 6.
+Check (false && I 3)%bool /\ (I 6)%bool.
 
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 1ec701ae81..a1028bda0c 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -41,7 +41,7 @@ Notation plus2 n := (S(S(n)))
 match n with
 | nil => 2
 | 0 :: _ => 2
-| list1 => 0
+| 1 :: nil => 0
 | 1 :: _ :: _ => 2
 | plus2 _ :: _ => 2
 end
@@ -84,3 +84,9 @@ a≡
      : Set
 .α
      : Set
+# a : .α =>
+# b : .α =>
+let res := 0 in
+for i from 0 to a updating (res)
+{{for j from 0 to b updating (res) {{S res}};; res}};; res
+     : .α -> .α -> .α
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index ceb29d1b9e..4c3eaa0c7b 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -70,6 +70,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
 (* Note: does not work for pattern *)
 Module A.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
+Open Scope nat_scope.
 Check fun f x => f x + S x.
 
 Open Scope list_scope.
@@ -145,3 +146,24 @@ Check .a≡.
 Notation ".α" := nat.
 Check nat.
 Check .α.
+
+(* A test for #6304 *)
+
+Module M6304.
+Notation "'for' m 'from' 0 'to' N 'updating' ( s1 )  {{ b }} ;; rest" :=
+  (let s1 :=
+    (fix rec(n: nat) := match n with
+     | 0 => s1
+     | S m => let s1 := rec m in b
+     end) N
+  in rest)
+  (at level 20).
+
+Check fun (a b : nat) =>
+  let res := 0 in
+  for i from 0 to a updating (res) {{
+    for j from 0 to b updating (res) {{ S res }};;
+    res
+  }};; res.
+
+End M6304.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 6ef75dd135..1b57252752 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -128,3 +128,13 @@ return (1, 2, 3, 4)
      : nat
 *(1.2)
      : nat
+[{0; 0}]
+     : list (list nat)
+[{1; 2; 3};
+ {4; 5; 6};
+ {7; 8; 9}]
+     : list (list nat)
+amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
+     : unit
+alist = [0; 1; 2]
+     : list nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 8c7bbe5917..a8d6c97fbd 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
 (* Notations with variables bound both as a term and as a binder      *)
 (* This is #4592 *)
 
-Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope.
 Check forall n:nat, {# n | 1 > n}.
 
 Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
@@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 
 (* Test spacing in #5569 *)
 
+Section S1.
+Variable plus : nat -> nat -> nat.
+Infix "+" := plus.
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+End S1.
 
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
@@ -193,7 +197,59 @@ Check !!! (x y:nat), True.
 
 (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
 
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Section S2.
+Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope.
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope.
 Check (((id 1) + 2) + 3).
 Check (id (1 + 2)).
+End S2.
+
+(* Test printing of notations guided by scope *)
+
+Module A.
+
+Delimit Scope line_scope with line.
+Notation "{ }" := nil (format "{ }") : line_scope.
+Notation "{ x }" := (cons x nil) : line_scope.
+Notation "{ x ; y ; .. ; z }" :=  (cons x (cons y .. (cons z nil) ..)) : line_scope.
+Notation "[ ]" := nil (format "[ ]") : matx_scope.
+Notation "[ l ]" := (cons l%line nil) : matx_scope.
+Notation "[ l ; l' ; .. ; l'' ]" :=  (cons l%line (cons l'%line .. (cons l''%line nil) ..))
+  (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope.
+
+Open Scope matx_scope.
+Check [[0;0]].
+Check [[1;2;3];[4;5;6];[7;8;9]].
+
+End A.
+
+(* Example by Beta Ziliani *)
+
+Require Import Lists.List.
+
+Module B.
+
+Import ListNotations.
+
+Delimit Scope pattern_scope with pattern.
+Delimit Scope patterns_scope with patterns.
+
+Notation "a => b" := (a, b) (at level 201) : pattern_scope.
+Notation "'with' p1 | .. | pn 'end'" :=
+  ((cons p1%pattern (.. (cons pn%pattern nil) ..)))
+    (at level 91, p1 at level 210, pn at level 210) : patterns_scope.
+
+Definition mymatch (n:nat) (l : list (nat * nat)) := tt.
+Arguments mymatch _ _%patterns.
+Notation "'mmatch' n ls" := (mymatch n ls) (at level 0).
+
+Close Scope patterns_scope.
+Close Scope pattern_scope.
+
+Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end.
+Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *)
+
+Definition alist := [0;1;2].
+Print alist.
+
+End B.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f69379a571..d6d410d1ae 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -44,26 +44,45 @@ bar@{u} = nat
 bar is universe polymorphic
 foo@{u Top.17 v} = 
 Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.17+1, v+1)}
+     : Type@{max(u+1,Top.17+1,v+1)}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
-Monomorphic mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic mono = Type@{mono.u}
+     : Type@{mono.u+1}
+(* {mono.u} |=  *)
 
 mono is not universe polymorphic
+mono
+     : Type@{mono.u+1}
+Type@{mono.u}
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+     : Type@{MONOU+1}
+mono.monomono
+     : Type@{mono.MONOU+1}
+monomono
+     : Type@{MONOU+1}
+mono
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane = 
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+     : Type@{max(tt.u,ff.u)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
-     : Type@{max(E+1, M+1, N+1)}
+     : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
 
 foo is universe polymorphic
 foo@{Top.16 Top.17 Top.18} = 
 Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
 (* Top.16 Top.17 Top.18 |=  *)
 
 foo is universe polymorphic
@@ -88,9 +107,10 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
 bind_univs.poly@{u} = Type@{u}
@@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
 insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
@@ -125,28 +145,28 @@ inmod@{u} = Type@{u}
 inmod is universe polymorphic
 Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.36} -> Type@{i}
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.36} -> Type@{i}
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 116d5e5e94..266d94ad99 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,6 +1,6 @@
 Set Universe Polymorphism.
 Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
 Inductive Empty@{u} : Type@{u} := .
@@ -25,14 +25,59 @@ Print wrap.
 Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
+Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+  Fail Monomorphic Universe u.
+  Monomorphic Universe MONOU.
+
+  Monomorphic Definition monomono := Type@{MONOU}.
+  Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+  Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+  Unset Universe Polymorphism.
+  Section foo.
+    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    Unset Strict Universe Declaration.
+    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Definition bobmorane := tt -> ff.
+  End foo.
+  Print bobmorane. (*
+                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
+                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(Top.15,ff.u)}
+                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     ff.v < ff.u
+                    *)
+
+                    bobmorane is universe polymorphic
+                    *)
+End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
 Fail Definition fo@{u u} := Type@{u}.
@@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
 Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
 
 (* Universe binders survive through compilation, sections and modules. *)
-Require bind_univs.
+Require TestSuite.bind_univs.
 Print bind_univs.mono.
 Print bind_univs.poly.
 
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index 172612405f..7326f137c2 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,20 +1,40 @@
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.foo" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.bar" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing arguments for variables y and _.
+The user-defined tactic "Top.bar" was not fully applied:
+There are missing arguments for variables y and _,
+an argument was provided for variable x.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.baz" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.qux" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+The user-defined tactic "Top.mydo" was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.rec" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable x,
+an argument was provided for variable tac.
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
index f17c00e9d7..e834fde113 100644
--- a/test-suite/prerequisite/bind_univs.v
+++ b/test-suite/prerequisite/bind_univs.v
@@ -3,3 +3,5 @@
 Monomorphic Definition mono@{u} := Type@{u}.
 
 Polymorphic Definition poly@{u} := Type@{u}.
+
+Monomorphic Universe reqU.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 6b1f0315bc..cd6eac35cf 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -240,3 +240,20 @@ Module IterativeDeepening.
   Qed.
 
 End IterativeDeepening.
+
+Module AxiomsAreInstances.
+  Set Typeclasses Axioms Are Instances.
+  Class TestClass1 := {}.
+  Axiom testax1 : TestClass1.
+  Definition testdef1 : TestClass1 := _.
+
+  Unset Typeclasses Axioms Are Instances.
+  Class TestClass2 := {}.
+  Axiom testax2 : TestClass2.
+  Fail Definition testdef2 : TestClass2 := _.
+
+  (* we didn't break typeclasses *)
+  Existing Instance testax2.
+  Definition testdef2 : TestClass2 := _.
+
+End AxiomsAreInstances.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 3178c6fc15..730b367d60 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -55,6 +55,7 @@ Module Backtracking.
     Axiom A : Type.
     Existing Class A.
     Axioms a b c d e: A.
+    Existing Instances a b c d e.
     
     Ltac get_value H := eval cbv delta [H] in H.
     
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
new file mode 100644
index 0000000000..c4a1d7c28f
--- /dev/null
+++ b/test-suite/success/unidecls.v
@@ -0,0 +1,121 @@
+Set Printing Universes.
+
+Module unidecls.
+  Universes a b.
+End unidecls.
+
+Universe a.
+
+Constraint a < unidecls.a.
+
+Print Universes.
+
+(** These are different universes *)
+Check Type@{a}.
+Check Type@{unidecls.a}.
+
+Check Type@{unidecls.b}.
+
+Fail Check Type@{unidecls.c}.
+
+Fail Check Type@{i}.
+Universe foo.
+Module Foo.
+  (** Already declared globaly: but universe names are scoped at the module level  *)
+  Universe foo.
+  Universe bar.
+
+  Check Type@{Foo.foo}.
+  Definition bar := 0.
+End Foo.
+
+(** Already declared in the module *)
+Universe bar.
+
+(** Accessible outside the module: universe declarations are global *)
+Check Type@{bar}.
+Check Type@{Foo.bar}.
+
+Check Type@{Foo.foo}.
+(** The same *)
+Check Type@{foo}.
+Check Type@{Top.foo}.
+
+Universe secfoo.
+Section Foo'.
+  Fail Universe secfoo.
+  Universe secfoo2.
+  Check Type@{Foo'.secfoo2}.
+  Constraint secfoo2 < a.
+End Foo'.
+
+Check Type@{secfoo2}.
+Fail Check Type@{Foo'.secfoo2}.
+Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
+
+(** Below, u and v are global, fixed universes *)
+Module Type Arg.
+  Universe u.
+  Parameter T: Type@{u}.
+End Arg.
+
+Module Fn(A : Arg).
+  Universes v.
+
+  Check Type@{A.u}.
+  Constraint A.u < v.
+
+  Definition foo : Type@{v} := nat.
+  Definition bar : Type@{A.u} := nat.
+
+  Fail Definition foo(A : Type@{v}) : Type@{A.u} := A.
+End Fn.
+
+Module ArgImpl : Arg.
+  Definition T := nat.
+End ArgImpl.
+
+Module ArgImpl2 : Arg.
+  Definition T := bool.
+End ArgImpl2.
+
+(** Two applications of the functor result in the exact same universes *)
+Module FnApp := Fn(ArgImpl).
+
+Check Type@{FnApp.v}.
+Check FnApp.foo.
+Check FnApp.bar.
+
+Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}).
+
+Module FnApp2 := Fn(ArgImpl).
+Check Type@{FnApp2.v}.
+Check FnApp2.foo.
+Check FnApp2.bar.
+
+Import ArgImpl2.
+(** Now u refers to ArgImpl.u and ArgImpl2.u *)
+Check FnApp2.bar.
+
+(** It can be shadowed *)
+Universe u.
+
+(** This refers to the qualified name *)
+Check FnApp2.bar.
+
+Constraint u = ArgImpl.u.
+Print Universes.
+
+Set Universe Polymorphism.
+
+Section PS.
+  Universe poly.
+
+  Definition id (A : Type@{poly}) (a : A) : A := a.
+End PS.
+(** The universe is polymorphic and discharged, does not persist *)
+Fail Check Type@{poly}.
+
+Print Universes.
+Check id nat.
+Check id@{Set}.