Fix interpretation of global universes in univdecl constraints.

Also nicer error when the constraints are impossible.

3 files changed, 10 insertions, 0 deletions

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a2857294b..9eb162fc0 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -86,6 +86,8 @@ The command has indeed failed with message:
 Universe instance should have length 0
 The command has indeed failed with message:
 This object does not support universe names.
+The command has indeed failed with message:
+Cannot enforce v < u because u < gU < gV < v
 Monomorphic bind_univs.mono = Type@{u}
      : Type@{u+1}
 (* {u} |=  *)
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 013f215b5..a65a1fdf3 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -56,6 +56,10 @@ Fail Print mono@{E}.
 (* Not everything can be printed with custom universe names. *)
 Fail Print Coq.Init.Logic@{E}.
 
+(* Nice error when constraints are impossible. *)
+Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
+Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require bind_univs.
 Print bind_univs.mono.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index c09a60a4d..b3f9a4994 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -202,6 +202,10 @@ Module binders.
     exact Type@{i}.
   Qed.
 
+  Monomorphic Universe M.
+  Fail Definition with_mono@{u|} : Type@{M} := Type@{u}.
+  Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
+
 End binders.
     
 Section cats.