5 files changed, 30 insertions, 10 deletions
diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v
new file mode 100644
index 0000000000..9be1936cdf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8791.v
@@ -0,0 +1,9 @@
+Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
+
+Definition A := 42.
+
+Instance foo (A: Type): Inhabited (list A).
+Check A.
+Abort.
+
+Fail Instance foo (A : nat) (A : Type) : Inhabited nat.
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index 6d8ce7c5d7..047f4cd080 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -15,7 +15,7 @@ let evil t f =
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
-      ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
       ~types:(Term.mkArrow tc tu)
       (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
   in
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 49c292c501..178116c580 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -150,6 +150,11 @@ Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
 For inseccstr: Argument scope is [type_scope]
+Polymorphic insec2@{u} = Prop
+     : Type@{Set+1}
+(* u |=  *)
+
+insec2 is universe polymorphic
 Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
@@ -171,26 +176,26 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i UnivBinders.55 UnivBinders.56} :
-Type@{UnivBinders.55} -> Type@{i}
-(* i UnivBinders.55 UnivBinders.56 |=  *)
+axfoo@{i UnivBinders.56 UnivBinders.57} :
+Type@{UnivBinders.56} -> Type@{i}
+(* i UnivBinders.56 UnivBinders.57 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.55 UnivBinders.56} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.55 UnivBinders.56 |=  *)
+axbar@{i UnivBinders.56 UnivBinders.57} :
+Type@{UnivBinders.57} -> Type@{i}
+(* i UnivBinders.56 UnivBinders.57 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i}
+axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i}
+axbar' : Type@{UnivBinders.59} -> 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 56474a0723..19d241d35d 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -130,6 +130,12 @@ End SomeSec.
 Print insec.
 Print insecind.
 
+Section SomeSec2.
+  Universe u.
+  Definition insec2@{} := Prop.
+End SomeSec2.
+Print insec2.
+
 Module SomeMod.
   Definition inmod@{u} := Type@{u}.
   Print inmod.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index ebf5b094e1..2f13b7c225 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -169,7 +169,7 @@ Proof.
 Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
                  (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
 
-Timeout 1 Fail apply _. (* 0.06s *)
+  Timeout 1 Fail apply _. (* 0.06s *)
 Abort.
 End HintCut.