diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
commit | 164c6861860e6b52818c031f901ffeff91fca16a (patch) | |
tree | 4f91d20c890c25915e7b28226c663b94a8cfb0d3 /test-suite/bugs/closed/4443.v | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'test-suite/bugs/closed/4443.v')
-rw-r--r-- | test-suite/bugs/closed/4443.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v new file mode 100644 index 00000000..66dfa0e6 --- /dev/null +++ b/test-suite/bugs/closed/4443.v @@ -0,0 +1,31 @@ +Set Universe Polymorphism. + +Record TYPE@{i} := cType { + type : Type@{i}; +}. + +Definition PROD@{i j k} + (A : Type@{i}) + (B : A -> Type@{j}) + : TYPE@{k}. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + +Local Unset Strict Universe Declaration. +Definition PRODinj + (A : Type@{i}) + (B : A -> Type) + : TYPE. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + + Monomorphic Universe i j. + Monomorphic Constraint j < i. +Set Printing Universes. +Check PROD@{i i i}. +Check PRODinj@{i j}. +Fail Check PRODinj@{j i}.
\ No newline at end of file |