summaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
d---------byterun402logplain
-rw-r--r--cbytecodes.ml3906logplain
-rw-r--r--cbytecodes.mli1710logplain
-rw-r--r--cbytegen.ml15606logplain
-rw-r--r--cbytegen.mli352logplain
-rw-r--r--cemitcodes.ml9031logplain
-rw-r--r--cemitcodes.mli939logplain
-rw-r--r--closure.ml37785logplain
-rw-r--r--closure.mli6690logplain
-rw-r--r--conv_oracle.ml1622logplain
-rw-r--r--conv_oracle.mli1354logplain
-rw-r--r--cooking.ml3632logplain
-rw-r--r--cooking.mli1113logplain
-rw-r--r--csymtable.ml4939logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml7954logplain
-rw-r--r--declarations.mli6337logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3163logplain
-rw-r--r--entries.mli3164logplain
-rw-r--r--environ.ml10212logplain
-rw-r--r--environ.mli8148logplain
-rw-r--r--esubst.ml4979logplain
-rw-r--r--esubst.mli1767logplain
-rw-r--r--indtypes.ml22236logplain
-rw-r--r--indtypes.mli1393logplain
-rw-r--r--inductive.ml33673logplain
-rw-r--r--inductive.mli3238logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml7596logplain
-rw-r--r--mod_subst.mli2796logplain
-rw-r--r--mod_typing.ml12086logplain
-rw-r--r--mod_typing.mli978logplain
-rw-r--r--modops.ml10254logplain
-rw-r--r--modops.mli3049logplain
-rw-r--r--names.ml8351logplain
-rw-r--r--names.mli5256logplain
-rw-r--r--pre_env.ml3820logplain
-rw-r--r--pre_env.mli2360logplain
-rw-r--r--reduction.ml14870logplain
-rw-r--r--reduction.mli2571logplain
-rw-r--r--safe_typing.ml16951logplain
-rw-r--r--safe_typing.mli3874logplain
-rw-r--r--sign.ml6394logplain
-rw-r--r--sign.mli3721logplain
-rw-r--r--subtyping.ml9482logplain
-rw-r--r--subtyping.mli727logplain
-rw-r--r--term.ml38404logplain
-rw-r--r--term.mli18215logplain
-rw-r--r--term_typing.ml3720logplain
-rw-r--r--term_typing.mli1110logplain
-rw-r--r--type_errors.ml3776logplain
-rw-r--r--type_errors.mli3499logplain
-rw-r--r--typeops.ml14731logplain
-rw-r--r--typeops.mli3132logplain
-rw-r--r--univ.ml16611logplain
-rw-r--r--univ.mli2120logplain
-rw-r--r--vconv.ml18057logplain
-rw-r--r--vconv.mli1372logplain
-rw-r--r--vm.ml15808logplain
-rw-r--r--vm.mli2510logplain