diff options
| author | Hugo Herbelin | 2014-11-03 20:20:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-04 16:34:12 +0100 |
| commit | bcba6d1bc9f769da593a3b01a12846f3e7a26a25 (patch) | |
| tree | f09be5662a73315b38a21f49afc0dd8b8407cf4b /lib | |
| parent | d1321c8d686cc0e392c8ae26beb8abe762258900 (diff) | |
Experimentally applying eager evar substitution at the same time as
eager meta substition in w_unify, so as to preserve compatibility
after PMP's move of (setoid) rewrite clauses from metas to
evars (fbbe491cfa).
Hoping it is compatible for non-rewrite uses of the eager meta flag,
and that it is not too costly.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions