diff options
| author | Matthieu Sozeau | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /_CoqProject | |
| parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) | |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions