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/4420.v | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5upstream/8.5
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. + |