diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-19 14:09:55 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-19 14:32:06 -0500 |
| commit | cbef33066dd526516c03474ffb35457047093808 (patch) | |
| tree | 1c2e36433957211c69a9915ef7d39b3aac5587e3 /test-suite/bugs/closed/4420.v | |
| parent | 13e969e644a6ad23f6d326f3e4a253ae0393da9c (diff) | |
Fix bug #4420: check_types was losing universe constraints.
Diffstat (limited to 'test-suite/bugs/closed/4420.v')
| -rw-r--r-- | test-suite/bugs/closed/4420.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4420.v b/test-suite/bugs/closed/4420.v new file mode 100644 index 000000000..0e16cb239 --- /dev/null +++ b/test-suite/bugs/closed/4420.v @@ -0,0 +1,19 @@ +Module foo. + Context (Char : Type). + Axiom foo : Type -> Type. + Goal foo Char = foo Char. + change foo with (fun x => foo x). + cbv beta. + reflexivity. + Defined. +End foo. + +Inductive foo (A : Type) : Prop := I. (*Top.1*) +Lemma bar : foo Type. (*Top.3*) +Proof. + Set Printing Universes. +change foo with (fun x : Type => foo x). (*Top.4*) +cbv beta. +apply I. (* I Type@{Top.3} : (fun x : Type@{Top.4} => foo x) Type@{Top.3} *) +Defined. + |