aboutsummaryrefslogtreecommitdiffhomepage
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.ml33565logplain
-rw-r--r--closure.mli6351logplain
-rw-r--r--conv_oracle.ml1570logplain
-rw-r--r--conv_oracle.mli1301logplain
-rw-r--r--cooking.ml3924logplain
-rw-r--r--cooking.mli1081logplain
-rw-r--r--csymtable.ml5260logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml8723logplain
-rw-r--r--declarations.mli6238logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2912logplain
-rw-r--r--entries.mli2929logplain
-rw-r--r--environ.ml20822logplain
-rw-r--r--environ.mli9387logplain
-rw-r--r--esubst.ml5582logplain
-rw-r--r--esubst.mli1906logplain
-rw-r--r--indtypes.ml24530logplain
-rw-r--r--indtypes.mli1355logplain
-rw-r--r--inductive.ml34560logplain
-rw-r--r--inductive.mli3945logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml13663logplain
-rw-r--r--mod_subst.mli3187logplain
-rw-r--r--mod_typing.ml12626logplain
-rw-r--r--mod_typing.mli1019logplain
-rw-r--r--modops.ml17295logplain
-rw-r--r--modops.mli3312logplain
-rw-r--r--names.ml8894logplain
-rw-r--r--names.mli5765logplain
-rw-r--r--pre_env.ml3743logplain
-rw-r--r--pre_env.mli2435logplain
-rw-r--r--reduction.ml17606logplain
-rw-r--r--reduction.mli2817logplain
-rw-r--r--retroknowledge.ml8314logplain
-rw-r--r--retroknowledge.mli5970logplain
-rw-r--r--safe_typing.ml24869logplain
-rw-r--r--safe_typing.mli4318logplain
-rw-r--r--sign.ml6611logplain
-rw-r--r--sign.mli3883logplain
-rw-r--r--subtyping.ml15154logplain
-rw-r--r--subtyping.mli676logplain
-rw-r--r--term.ml38423logplain
-rw-r--r--term.mli18616logplain
-rw-r--r--term_typing.ml4404logplain
-rw-r--r--term_typing.mli1340logplain
-rw-r--r--type_errors.ml3799logplain
-rw-r--r--type_errors.mli3548logplain
-rw-r--r--typeops.ml16400logplain
-rw-r--r--typeops.mli3556logplain
-rw-r--r--univ.ml19068logplain
-rw-r--r--univ.mli2729logplain
-rw-r--r--vconv.ml7758logplain
-rw-r--r--vconv.mli841logplain
-rw-r--r--vm.ml19400logplain
-rw-r--r--vm.mli2304logplain