4 files changed, 74 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v
new file mode 100644
index 0000000000..10f955b41f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8364.v
@@ -0,0 +1,17 @@
+Unset Primitive Projections.
+
+Record Box (A:Type) := box { unbox : A }.
+Arguments box {_} _. Arguments unbox {_} _.
+
+Definition map {A B} (f:A -> B) x :=
+  match x with box x => box (f x) end.
+
+Definition tuple (l : Box Type) : Type :=
+  match l with
+  | box x => x
+  end.
+
+Fail Inductive stack : Type -> Type :=
+| Stack T foos :
+  tuple (map stack foos) ->
+  stack T.
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d2116d2183..95daa1bb0c 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -2,7 +2,7 @@ Definition T := nat.
 
 Definition le := le.
 
-Hint Unfold le.
+Hint Unfold le : core.
 
 Lemma le_refl : forall n : nat, le n n.
   auto.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index d76b307914..339f798240 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -165,19 +165,13 @@ Module binders.
     exact A.
   Defined.
 
-  Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}.
-    pose(foo:=Type).
-    exact A.
-    Fail Defined.
-  Abort.
-
-  Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}.
-    pose(foo:=Type).
-    exact A.
-  Defined.
+  Polymorphic Lemma hidden_strict_type : Type.
+  Proof.
+    exact Type.
+  Qed.
+  Check hidden_strict_type@{_}.
+  Fail Check hidden_strict_type@{Set}.
 
-  Check moreu@{_ _ _ _}.
-  
   Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A.
 
   (* By default constraints are extensible *)
diff --git a/test-suite/success/private_univs.v b/test-suite/success/private_univs.v
new file mode 100644
index 0000000000..5c30b33435
--- /dev/null
+++ b/test-suite/success/private_univs.v
@@ -0,0 +1,50 @@
+Set Universe Polymorphism. Set Printing Universes.
+
+Definition internal_defined@{i j | i < j +} (A : Type@{i}) : Type@{j}.
+  pose(foo:=Type). (* 1 universe for the let body + 1 for the type *)
+  exact A.
+  Fail Defined.
+Abort.
+
+Definition internal_defined@{i j +} (A : Type@{i}) : Type@{j}.
+pose(foo:=Type).
+exact A.
+Defined.
+Check internal_defined@{_ _ _ _}.
+
+Module M.
+Lemma internal_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (foo := Type).
+  exact A.
+Qed.
+Check internal_qed@{_ _}.
+End M.
+Include M.
+(* be careful to remove const_private_univs in Include! will be coqchk'd *)
+
+Unset Strict Universe Declaration.
+Lemma private_transitivity@{i j} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (bar := Type : Type@{j}).
+  pose (foo := Type@{i} : bar).
+  exact bar.
+Qed.
+
+Definition private_transitivity'@{i j|i < j} := private_transitivity@{i j}.
+Fail Definition dummy@{i j|j <= i +} := private_transitivity@{i j}.
+
+Unset Private Polymorphic Universes.
+Lemma internal_noprivate_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (foo := Type).
+  exact A.
+  Fail Qed.
+Abort.
+
+Lemma internal_noprivate_qed@{i j +} (A:Type@{i}) : Type@{j}.
+Proof.
+  pose (foo := Type).
+  exact A.
+Qed.
+Check internal_noprivate_qed@{_ _ _ _}.