diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-28 19:43:58 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-28 19:50:30 +0100 |
| commit | 15aeb84a0deb444af81f4035dbcf791566bafe5f (patch) | |
| tree | ba7fb0a866f759577ff6b1437cb62b6b24c40985 /test-suite/bugs/closed/3807.v | |
| parent | 90fef3ffd236f2ed5575b0d11a47185185abc75b (diff) | |
Closed bugs.
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 000000000..108ebf592 --- /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 |