From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/7695.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 test-suite/bugs/closed/7695.v (limited to 'test-suite/bugs/closed/7695.v') diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v new file mode 100644 index 00000000..42bdb076 --- /dev/null +++ b/test-suite/bugs/closed/7695.v @@ -0,0 +1,20 @@ +Require Import Hurkens. + +Universes i j k. +Module Type T. + Parameter T1 : Type@{i+1}. + Parameter e : Type@{j} = T1 : Type@{k}. +End T. + +Module M. + Definition T1 := Type@{j}. + Definition e : Type@{j} = T1 : Type@{k} := eq_refl. +End M. + +Module F (A:T). + Definition bad := TypeNeqSmallType.paradox _ A.e. +End F. + +Set Printing Universes. +Fail Module X := F M. +(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *) -- cgit v1.2.3