aboutsummaryrefslogtreecommitdiff
path: root/kernel/cooking.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-09-03 12:41:46 +0200
committerMaxime Dénès2018-09-03 12:41:46 +0200
commitda58ae4c620412923ea84b1982e8765f6be145a8 (patch)
tree8518269959c007a7c70bdbd80a968ebff03c6415 /kernel/cooking.ml
parent3bc0c82700a805e889198b810cc0148f6479cbe1 (diff)
parent568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 (diff)
Merge PR #7912: Simplify effects API
Diffstat (limited to 'kernel/cooking.ml')
0 files changed, 0 insertions, 0 deletions