aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-05-16 17:41:03 +0200
committerPierre-Marie Pédrot2018-10-16 10:58:17 +0200
commitf113e4c5ddbc3b13c589b8384120837465af76fa (patch)
tree6f0e689f94421054e40f3c154d2ea75066e36f79 /kernel/nativecode.mli
parent697a59de8a39f3a4b253ced93ece1209b7f0eb1b (diff)
Document the issue with positive coinductive types.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions