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 | |
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')
0 files changed, 0 insertions, 0 deletions