6 files changed, 46 insertions, 26 deletions
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
index 4f29b76c6e..dce73e1a50 100644
--- a/test-suite/bugs/closed/3446.v
+++ b/test-suite/bugs/closed/3446.v
@@ -1,28 +1,32 @@
 (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
-(* Set Asymmetric Patterns. *)
-(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *)
-(* Notation "A -> B" := (forall (_ : A), B). *)
+Module First.
+Set Asymmetric Patterns.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B).
+Set Universe Polymorphism.
+
 
-(* Notation "x → y" := (x -> y) *)
-(*   (at level 99, y at level 200, right associativity): type_scope. *)
-(* Record sigT A (P : A -> Type) := *)
-(*   { projT1 : A ; projT2 : P projT1 }. *)
-(* Arguments projT1 {A P} s. *)
-(* Arguments projT2 {A P} s. *)
-(* Set Universe Polymorphism. *)
-(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *)
-(* Reserved Notation "x = y" (at level 70, no associativity). *)
-(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *)
-(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *)
-(* Reserved Notation "{ x : A  & P }" (at level 0, x at level 99). *)
-(* Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope. *)
+Notation "x → y" := (x -> y)
+  (at level 99, y at level 200, right associativity): type_scope.
+Record sigT A (P : A -> Type) :=
+  { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} s.
+Arguments projT2 {A P} s.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Reserved Notation "x = y" (at level 70, no associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y).
+Notation " x = y " := (paths x y) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope.
 
 
-(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v. *)
-(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *)
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v.
+Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}).
 
-(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *)
-(*   @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *)
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) :=
+  @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _).
+End First.
 
 Set Asymmetric Patterns.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 9320848910..0ccc92067d 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1).
 Monomorphic Axiom dummy_funext_type : Type0.
 Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Record TruncType (n : trunc_index) := BuildTruncType {
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index 1449f242b4..c6cb9c35e6 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
 
 Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Ltac done :=
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 6efd671a8c..b1558dab1c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -70,7 +70,7 @@ FST (0; 1)
      : Z
 Nil
      : forall A : Type, list A
-NIL:list nat
+NIL : list nat
      : list nat
 (false && I 3)%bool /\ I 6
      : Prop
@@ -78,7 +78,7 @@ NIL:list nat
      : Z * Z * Z * (Z * Z * Z)
 [|0 * (1, 2, 3); (4, 5, 6) * false|]
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
-fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
      : (Z -> Z -> Z -> Z) -> Z
 Init.Nat.add
      : nat -> nat -> nat
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index b1952aecf5..f2d1447785 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,12 +6,12 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n in ?y ?y0:T n
+fun n : nat => let x := A n in ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat  x := A n : T n |- ?T0 -> T n] 
 ?y0 : [n : nat  x := A n : T n |- ?T0] 
-fun n : nat => ?y ?y0:T n
+fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat |- ?T0 -> T n] 
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9167c9fcbf..dc22b03f2d 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -292,3 +292,19 @@ Section foo2.
   Context `{forall A B, Funext A B}.
   Print Universes.
 End foo2.
+
+Module eta.
+Set Universe Polymorphism.
+
+Set Printing Universes.
+
+Axiom admit : forall A, A.
+Record R := {O : Type}.
+
+Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
+Definition RLRL' : forall x : R, RL x = RL (RL x).
+  intros. apply eq_refl.
+Qed.
+
+End eta.