diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:05:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:13:30 +0100 |
| commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
| tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /test-suite/bugs/closed/3807.v | |
| parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
| parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) | |
Merge branch 'v8.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 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 |