diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-13 16:37:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-13 17:08:13 +0200 |
| commit | bb43103f7ecea16e634d448215f24d6d55d56eb1 (patch) | |
| tree | 7de6b19bfc24428b90a48323e0d36c837df34ce4 /library/lib.ml | |
| parent | 87be9070b3415f31027b78165b213de34c168043 (diff) | |
evar_conv: Refine occur_rigidly
This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
Diffstat (limited to 'library/lib.ml')
0 files changed, 0 insertions, 0 deletions