diff options
| author | Matthieu Sozeau | 2015-11-24 15:48:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-24 15:50:32 +0100 |
| commit | 2d32a2c5606286c85fd35c7ace167b4d4e108ced (patch) | |
| tree | 43dd55e9ff642f92ad045864126f64e24a2436af /kernel/inductive.ml | |
| parent | 1467c22548453cd07ceba0029e37c8bbdfd039ea (diff) | |
Univs: carry on universe substitution when defining obligations of
non-polymorphic definitions, original universes might be substituted
later on due to constraints.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions