diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-20 00:27:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:29:06 +0100 |
| commit | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (patch) | |
| tree | 5b68a2bd48fc961987a193f4361c46f7b9940b33 /engine/eConstr.mli | |
| parent | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (diff) | |
Cumulativity: improve treatment of irrelevant universes.
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
Diffstat (limited to 'engine/eConstr.mli')
0 files changed, 0 insertions, 0 deletions