diff options
| author | Matthieu Sozeau | 2014-11-22 19:34:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-11-23 15:28:41 +0100 |
| commit | ff0a051caf031fb427007714f6325c74b8893702 (patch) | |
| tree | fbb4b2fae772c9a0fe6a8b5d7310eb60dae7c045 /dev/include | |
| parent | c81065e5cdc6d803bd67eccf93dc8fbb640c6892 (diff) | |
Pass around information on the use of template polymorphism for
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions