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.ml2583logplain
-rw-r--r--conv_oracle.mli1513logplain
-rw-r--r--cooking.ml3924logplain
-rw-r--r--cooking.mli1081logplain
-rw-r--r--csymtable.ml5260logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml8790logplain
-rw-r--r--declarations.mli6334logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2912logplain
-rw-r--r--entries.mli2929logplain
-rw-r--r--environ.ml22291logplain
-rw-r--r--environ.mli9386logplain
-rw-r--r--esubst.ml5582logplain
-rw-r--r--esubst.mli2706logplain
-rw-r--r--indtypes.ml24741logplain
-rw-r--r--indtypes.mli1355logplain
-rw-r--r--inductive.ml34695logplain
-rw-r--r--inductive.mli4057logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml13663logplain
-rw-r--r--mod_subst.mli3187logplain
-rw-r--r--mod_typing.ml14195logplain
-rw-r--r--mod_typing.mli1076logplain
-rw-r--r--modops.ml17984logplain
-rw-r--r--modops.mli3312logplain
-rw-r--r--names.ml9110logplain
-rw-r--r--names.mli5917logplain
-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.ml25933logplain
-rw-r--r--safe_typing.mli4318logplain
-rw-r--r--sign.ml6611logplain
-rw-r--r--sign.mli3883logplain
-rw-r--r--subtyping.ml15710logplain
-rw-r--r--subtyping.mli676logplain
-rw-r--r--term.ml38728logplain
-rw-r--r--term.mli18809logplain
-rw-r--r--term_typing.ml4405logplain
-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.ml19501logplain
-rw-r--r--univ.mli2839logplain
-rw-r--r--vconv.ml7758logplain
-rw-r--r--vconv.mli841logplain
-rw-r--r--vm.ml19400logplain
-rw-r--r--vm.mli2304logplain