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/3807.v | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'test-suite/bugs/closed/3807.v')
-rw-r--r-- | test-suite/bugs/closed/3807.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v new file mode 100644 index 00000000..108ebf59 --- /dev/null +++ b/test-suite/bugs/closed/3807.v @@ -0,0 +1,33 @@ +Set Universe Polymorphism. +Set Printing Universes. +Unset Universe Minimization ToSet. + + +Definition foo : Type := nat. +About foo. +(* foo@{Top.1} : Type@{Top.1}*) +(* Top.1 |= *) + +Definition bar : foo -> nat. +Admitted. +About bar. +(* bar@{Top.2} : foo@{Top.2} -> nat *) +(* Top.2 |= *) + +Lemma baz@{i} : foo@{i} -> nat. +Proof. + exact bar. +Defined. + +Definition bar'@{i} : foo@{i} -> nat. + intros f. exact 0. +Admitted. +About bar'. +(* bar'@{i} : foo@{i} -> nat *) +(* i |= *) + +Axiom f@{i} : Type@{i}. +(* +*** [ f@{i} : Type@{i} ] +(* i |= *) +*)
\ No newline at end of file |