summaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
d---------byterun484logplain
-rw-r--r--cbytecodes.ml8959logplain
-rw-r--r--cbytecodes.mli5498logplain
-rw-r--r--cbytegen.ml32981logplain
-rw-r--r--cbytegen.mli1719logplain
-rw-r--r--cemitcodes.ml11212logplain
-rw-r--r--cemitcodes.mli939logplain
-rw-r--r--closure.ml33613logplain
-rw-r--r--closure.mli6401logplain
-rw-r--r--conv_oracle.ml2634logplain
-rw-r--r--conv_oracle.mli1565logplain
-rw-r--r--cooking.ml3973logplain
-rw-r--r--cooking.mli1130logplain
-rw-r--r--csymtable.ml5260logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml8777logplain
-rw-r--r--declarations.mli6293logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2961logplain
-rw-r--r--entries.mli2979logplain
-rw-r--r--environ.ml22408logplain
-rw-r--r--environ.mli9454logplain
-rw-r--r--esubst.ml5627logplain
-rw-r--r--esubst.mli1952logplain
-rw-r--r--indtypes.ml24580logplain
-rw-r--r--indtypes.mli1406logplain
-rw-r--r--inductive.ml34611logplain
-rw-r--r--inductive.mli3994logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml13714logplain
-rw-r--r--mod_subst.mli3239logplain
-rw-r--r--mod_typing.ml12732logplain
-rw-r--r--mod_typing.mli1129logplain
-rw-r--r--modops.ml17476logplain
-rw-r--r--modops.mli3361logplain
-rw-r--r--names.ml8940logplain
-rw-r--r--names.mli5812logplain
-rw-r--r--pre_env.ml3792logplain
-rw-r--r--pre_env.mli2485logplain
-rw-r--r--reduction.ml17655logplain
-rw-r--r--reduction.mli2869logplain
-rw-r--r--retroknowledge.ml8370logplain
-rw-r--r--retroknowledge.mli6027logplain
-rw-r--r--safe_typing.ml25800logplain
-rw-r--r--safe_typing.mli4372logplain
-rw-r--r--sign.ml6655logplain
-rw-r--r--sign.mli3929logplain
-rw-r--r--subtyping.ml15753logplain
-rw-r--r--subtyping.mli728logplain
-rw-r--r--term.ml38469logplain
-rw-r--r--term.mli18663logplain
-rw-r--r--term_typing.ml4457logplain
-rw-r--r--term_typing.mli1393logplain
-rw-r--r--type_errors.ml3851logplain
-rw-r--r--type_errors.mli3601logplain
-rw-r--r--typeops.ml16449logplain
-rw-r--r--typeops.mli3606logplain
-rw-r--r--univ.ml19391logplain
-rw-r--r--univ.mli2826logplain
-rw-r--r--vconv.ml7758logplain
-rw-r--r--vconv.mli841logplain
-rw-r--r--vm.ml19443logplain
-rw-r--r--vm.mli2304logplain