diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-03-09 15:15:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-03-09 16:23:05 +0100 |
| commit | a5ae3b2856e6cc6683652a0abb5a84b9787527c0 (patch) | |
| tree | dc9cccac803a02f1c2e45cfa87a67a95dee0c538 /lib/spawn.ml | |
| parent | d34a2ff176c75ea404f7eb638b6eea3ca07ab978 (diff) | |
Fix strategy of Keyed Unification
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
Diffstat (limited to 'lib/spawn.ml')
0 files changed, 0 insertions, 0 deletions