diff options
| author | Matthieu Sozeau | 2014-08-10 18:11:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-10 18:11:36 +0200 |
| commit | 519d2b0e5d6b53c2f2a02ee9b685088fd74be0f6 (patch) | |
| tree | a60c71949808ebffdabeb1b1701bbe6eb7824200 /plugins | |
| parent | 849c8d58f01618c06bca46a4532db8e288e6f703 (diff) | |
Fix bug introduced by earlier commit on first-order unification of primitive
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions