diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-22 10:17:39 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-22 11:11:48 +0200 |
| commit | 379c2403b1cd031091a2271353f26ab24afeb1e5 (patch) | |
| tree | ae367ef34e8b13e20dbff903e1f7e0a4d8c28e28 /proofs/refine.mli | |
| parent | c28a2a3a1297098ee73ad5b26e714164b6167d2b (diff) | |
Port fix for bugs 4763, 5149, previously 0b417c12e
Adds a compatibility flag so that the behavior of 8.5 can be obtained too.
Original commit:
unification.ml: fix for bug #4763, unif regression
Do not force all remaining conversions problems to be solved after
the _first_ solution of an evar. This was hell to track down, thanks
for the help of Maxime. contribs pass and HoTT too.
Diffstat (limited to 'proofs/refine.mli')
0 files changed, 0 insertions, 0 deletions