aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-10-25 14:58:39 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-10-25 14:58:39 +0100
commit83e82ef7b42f47d63d3b40b2698695a0e7b2d685 (patch)
treeef1ab4f39e6aec01d6ab5a37beed8709204711ac /library/declaremods.ml
parentc2de48c3f59415eaf0f2cbb5cfe78f23e908a459 (diff)
Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)
Diffstat (limited to 'library/declaremods.ml')
0 files changed, 0 insertions, 0 deletions