aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-03-09 16:43:49 +0100
committerMatthieu Sozeau2016-03-09 16:43:49 +0100
commitc633bb322acf0bb626eafe6158287d1ddc11af26 (patch)
treedb842a43a788e0a1e24fa27b63e7d9852b3c1666 /kernel/nativelambda.mli
parentccd7c003ae56a4f7ad600cfc9532651010fb6bf2 (diff)
Redo fix init_setoid -> init_relation_classes
It got lost during a merge with the 8.5 branch.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions