Merge PR #8850: Private universes for opaque polymorphic constants.

2 files changed, 56 insertions, 12 deletions

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@{_ _ _ _}.