aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-07-09 16:58:06 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-07-09 17:03:28 +0200
commit2c59d19ad207a6bf193e9f0c9d73258b3133d484 (patch)
tree36b64715df91a25e13ca950f5004815976bba371 /library/declaremods.mli
parente1f5a499c43ec0d7b7ebe696941217fb503e2596 (diff)
Kernel/Checker: Cleanup fixes of substitutions due to let-ins.
Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/
Diffstat (limited to 'library/declaremods.mli')
0 files changed, 0 insertions, 0 deletions