aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-04-22 17:39:42 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-04-22 18:55:13 +0200
commit74d7dd7ae08dedfd80c056a345c1b3398eb91b5e (patch)
treee8f7f71ebe8caccaaed72c89ea3863ff0701cab4 /kernel/constr.mli
parentb4552eb74c7ee577339b44924b59c2ab25f893d2 (diff)
Pp: obsolete comment.
Diffstat (limited to 'kernel/constr.mli')
0 files changed, 0 insertions, 0 deletions