diff options
| author | Matthieu Sozeau | 2015-11-20 20:18:11 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-20 20:19:16 +0100 |
| commit | 8d93301045c45ec48c85ecae2dfb3609e5e4695f (patch) | |
| tree | f0d9fdf1d8562d3ee5d1a3fdb82c96dd4acdca09 /kernel/reduction.ml | |
| parent | 2b47c0d1b492424c39477f9d4ec262e4d093be92 (diff) | |
Univs: generation of induction schemes should not generated useless
instances for each of the inductive in the same block but reuse the
original universe context shared by all of them. Also do not force
schemes to become universe polymorphic.
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions