aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-12-09 12:30:32 +0100
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-12-17 13:56:14 +0100
commit39b13903e7a6824f4405f61bb4b41a30cfbd0b3c (patch)
treeb0fb3df8a01b481283ccaa08092a351b70ac2191 /pretyping/reductionops.mli
parent597e5dd737dd235222798153b2342ae609519348 (diff)
CLEANUP: in the Reduction module
Diffstat (limited to 'pretyping/reductionops.mli')
0 files changed, 0 insertions, 0 deletions