Fix interpretation of global universes in univdecl constraints.

Also nicer error when the constraints are impossible.

2 files changed, 6 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.