diff options
author | 2014-11-23 12:49:25 +0100 | |
---|---|---|
committer | 2014-11-23 13:38:29 +0100 | |
commit | b3b3bbe6a0c0693c2a4e154685d109282d4b6f07 (patch) | |
tree | 94860b7e6581f680b93bfb9c887df485577a6782 /myocamlbuild.ml | |
parent | 00a05aea070121103baba2c03485127369f24538 (diff) |
Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about
when the arguments of a constructor can be moved at the place of the
variable on which destruct or induction applies.
Diffstat (limited to 'myocamlbuild.ml')
0 files changed, 0 insertions, 0 deletions