aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2016-10-27 14:14:50 +0200
committerMatthieu Sozeau2016-11-03 16:26:40 +0100
commit919545d39c77a9168e70141e78d2c9589dad7c4e (patch)
tree9bc2eda4f2f8c7bd1eceb0649898ad2ffc71b4e5 /kernel/cemitcodes.mli
parentf6916774eea2ecc1262377cb14c2d494a0486358 (diff)
Internal API change to typeclasses eauto.
This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking.
Diffstat (limited to 'kernel/cemitcodes.mli')
0 files changed, 0 insertions, 0 deletions