aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
authorHugo Herbelin2015-10-04 08:47:15 +0200
committerHugo Herbelin2015-12-10 09:35:05 +0100
commit75896eaaf60ce947e1fbc5a795ca5969bb1e4fae (patch)
treec9b000ca8676a1f2906890ce3db947334bf2a923 /kernel/cbytecodes.mli
parentcd31e372c6fb25769c26879f2f65f1937d098b87 (diff)
RefMan, ch. 4: Dropping the "Co" which noone uses in "(Co)Inductive".
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions