diff options
| author | Matthieu Sozeau | 2015-12-03 19:08:51 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-12-03 19:10:32 +0100 |
| commit | f41968d8c240db4653d0b9fe76e1646cd7c6fb68 (patch) | |
| tree | 04d051d79f853a86df3caedd435def2f09ac779f /test-suite/bugs | |
| parent | 281bed69ee7d4a7638d07f07f9d6722b897f29cc (diff) | |
Univs: fix bug #4443.
Do not substitute rigid variables during minimization, keeping
their equality constraints instead.
Diffstat (limited to 'test-suite/bugs')
| -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 0000000000..66dfa0e685 --- /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 |