diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-10 21:23:51 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-10 21:23:51 +0200 |
| commit | d65496f09c4b68fa318783e53f9cd6d5c18e1eb7 (patch) | |
| tree | 2b2aed815f4c2c987e9744978d6ef0bde305b8f4 /kernel/indtypes.mli | |
| parent | d0cd27e209be08ee51a2d609157367f053438a10 (diff) | |
Do not expand primitive projections eagerly in evarconv, but only
in cases of unification with existentials requiring it.
Diffstat (limited to 'kernel/indtypes.mli')
0 files changed, 0 insertions, 0 deletions