aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun526logplain
-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.ml33448logplain
-rw-r--r--closure.mli6481logplain
-rw-r--r--conv_oracle.ml2314logplain
-rw-r--r--conv_oracle.mli1513logplain
-rw-r--r--cooking.ml3915logplain
-rw-r--r--cooking.mli1081logplain
-rw-r--r--csymtable.ml5255logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml8929logplain
-rw-r--r--declarations.mli6422logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2660logplain
-rw-r--r--entries.mli2676logplain
-rw-r--r--environ.ml22517logplain
-rw-r--r--environ.mli9524logplain
-rw-r--r--esubst.ml5582logplain
-rw-r--r--esubst.mli2706logplain
-rw-r--r--indtypes.ml24871logplain
-rw-r--r--indtypes.mli1390logplain
-rw-r--r--inductive.ml34810logplain
-rw-r--r--inductive.mli4171logplain
-rw-r--r--kernel.mllib278logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml13701logplain
-rw-r--r--mod_subst.mli3187logplain
-rw-r--r--mod_typing.ml14195logplain
-rw-r--r--mod_typing.mli1076logplain
-rw-r--r--modops.ml18090logplain
-rw-r--r--modops.mli3312logplain
-rw-r--r--names.ml8998logplain
-rw-r--r--names.mli5917logplain
-rw-r--r--pre_env.ml3738logplain
-rw-r--r--pre_env.mli2435logplain
-rw-r--r--reduction.ml18348logplain
-rw-r--r--reduction.mli3146logplain
-rw-r--r--retroknowledge.ml8238logplain
-rw-r--r--retroknowledge.mli5970logplain
-rw-r--r--safe_typing.ml25956logplain
-rw-r--r--safe_typing.mli4318logplain
-rw-r--r--sign.ml2534logplain
-rw-r--r--sign.mli2335logplain
-rw-r--r--subtyping.ml15663logplain
-rw-r--r--subtyping.mli676logplain
-rw-r--r--term.ml43432logplain
-rw-r--r--term.mli21008logplain
-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.mli3551logplain
-rw-r--r--univ.ml19833logplain
-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