diff options
| author | Pierre-Marie Pédrot | 2014-03-03 14:20:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-03 15:26:51 +0100 |
| commit | 96f8d358c7d3c9a08ff2006f42716bc64937dad2 (patch) | |
| tree | c7a6503e6b39681aee60e556827614b5b3512778 /plugins/extraction/mlutil.ml | |
| parent | 49a764bd81ac1b21130d54a1808ce95b9992a36d (diff) | |
Fixing pervasive equalities. In particular, I removed the code that deleted
duplicates in kernel side effects. They were chosen according to an equality
that was quite irrelevant, and as expected this patch did not break the
test-suite.
Diffstat (limited to 'plugins/extraction/mlutil.ml')
0 files changed, 0 insertions, 0 deletions