diff options
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 00000000..0e16cb23 --- /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. + |