4 files changed, 74 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v
new file mode 100644
index 0000000000..261092ee6d
--- /dev/null
+++ b/test-suite/bugs/closed/5180.v
@@ -0,0 +1,64 @@
+Universes a b c ω ω'.
+Definition Typeω := Type@{ω}.
+Definition Type2 : Typeω := Type@{c}.
+Definition Type1 : Type2 := Type@{b}.
+Definition Type0 : Type1 := Type@{a}.
+
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Definition Typei' (n : nat)
+  := match n return Type@{ω'} with
+     | 0 => Type0
+     | 1 => Type1
+     | 2 => Type2
+     | _ => Typeω
+     end.
+Definition TypeOfTypei' {n} (x : Typei' n) : Type@{ω'}
+  := match n return Typei' n -> Type@{ω'} with
+     | 0 | 1 | 2 | _ => fun x => x
+     end x.
+Definition Typei (n : nat) : Typei' (S n)
+  := match n return Typei' (S n) with
+     | 0 => Type0
+     | 1 => Type1
+     | _ => Type2
+     end.
+Definition TypeOfTypei {n} (x : TypeOfTypei' (Typei n)) : Type@{ω'}
+  := match n return TypeOfTypei' (Typei n) -> Type@{ω'} with
+     | 0 | 1 | _ => fun x => x
+     end x.
+Check Typei 0 : Typei 1.
+Check Typei 1 : Typei 2.
+
+Definition lift' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => (x : Type)
+     end.
+Definition lift'' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => x
+     end. (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+Check (fun x : TypeOfTypei' (Typei 0) => TypeOfTypei' (Typei 1)).
+
+Definition lift''' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)).
+  refine match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))  with
+         | 0 | 1 | 2 | _ => fun x => _
+         end.
+  exact x.
+  Undo.
+  (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+  all:compute in *.
+  all:exact x.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v
new file mode 100644
index 0000000000..e29ebfb4ec
--- /dev/null
+++ b/test-suite/bugs/closed/5188.v
@@ -0,0 +1,5 @@
+Set Printing All.
+Axiom relation : forall (T : Type), Set.
+Axiom T : forall A (R : relation A), Set.
+Set Printing Universes.
+Parameter (A:_) (R:_) (e:@T A R).
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 9949658c44..239edd1da3 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
 Ltac f H := split; [ a H | e H ]
 Ltac g := match goal with
-          | |- context [if ?X then _ else _] => case X
+          | |- context [ if ?X then _ else _ ] => case X
           end
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index f62427ef47..6b1f0315bc 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -98,7 +98,7 @@ Goal exists R, @Refl nat R.
   solve [typeclasses eauto with foo].
 Qed.
 
-(* Set Typeclasses Compatibility "8.5". *)
+Set Typeclasses Compatibility "8.5".
 Parameter f : nat -> Prop.
 Parameter g : nat -> nat -> Prop.
 Parameter h : nat -> nat -> nat -> Prop.
@@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y.
 Hint Resolve a b c : mybase.
 Goal forall x y z, h x y z -> f x -> f y.
   intros.
-  Set Typeclasses Debug.
-  typeclasses eauto with mybase.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
   Unshelve.
 Abort.
 End bt.
@@ -138,7 +137,8 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Set Typeclasses Debug.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
 
 Goal forall `{B T}, Prop.
   intros. apply a.