summaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
d---------byterun402logplain
-rw-r--r--cbytecodes.ml4371logplain
-rw-r--r--cbytecodes.mli1944logplain
-rw-r--r--cbytegen.ml22536logplain
-rw-r--r--cbytegen.mli352logplain
-rw-r--r--cemitcodes.ml10239logplain
-rw-r--r--cemitcodes.mli939logplain
-rw-r--r--closure.ml37044logplain
-rw-r--r--closure.mli6605logplain
-rw-r--r--conv_oracle.ml1622logplain
-rw-r--r--conv_oracle.mli1354logplain
-rw-r--r--cooking.ml3900logplain
-rw-r--r--cooking.mli1120logplain
-rw-r--r--csymtable.ml4939logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml8873logplain
-rw-r--r--declarations.mli6707logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3163logplain
-rw-r--r--entries.mli3164logplain
-rw-r--r--environ.ml11274logplain
-rw-r--r--environ.mli8286logplain
-rw-r--r--esubst.ml5627logplain
-rw-r--r--esubst.mli1952logplain
-rw-r--r--indtypes.ml24382logplain
-rw-r--r--indtypes.mli1393logplain
-rw-r--r--inductive.ml34184logplain
-rw-r--r--inductive.mli3994logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml9103logplain
-rw-r--r--mod_subst.mli2796logplain
-rw-r--r--mod_typing.ml12099logplain
-rw-r--r--mod_typing.mli978logplain
-rw-r--r--modops.ml10706logplain
-rw-r--r--modops.mli3216logplain
-rw-r--r--names.ml8606logplain
-rw-r--r--names.mli5487logplain
-rw-r--r--pre_env.ml3949logplain
-rw-r--r--pre_env.mli2481logplain
-rw-r--r--reduction.ml15340logplain
-rw-r--r--reduction.mli2571logplain
-rw-r--r--safe_typing.ml18332logplain
-rw-r--r--safe_typing.mli3882logplain
-rw-r--r--sign.ml6544logplain
-rw-r--r--sign.mli3929logplain
-rw-r--r--subtyping.ml15926logplain
-rw-r--r--subtyping.mli727logplain
-rw-r--r--term.ml38547logplain
-rw-r--r--term.mli18724logplain
-rw-r--r--term_typing.ml4489logplain
-rw-r--r--term_typing.mli1379logplain
-rw-r--r--type_errors.ml3795logplain
-rw-r--r--type_errors.mli3539logplain
-rw-r--r--typeops.ml16367logplain
-rw-r--r--typeops.mli3582logplain
-rw-r--r--univ.ml17398logplain
-rw-r--r--univ.mli2273logplain
-rw-r--r--vconv.ml7758logplain
-rw-r--r--vconv.mli841logplain
-rw-r--r--vm.ml18861logplain
-rw-r--r--vm.mli2304logplain