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.ml3924logplain
-rw-r--r--cooking.mli1081logplain
-rw-r--r--csymtable.ml5255logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml8790logplain
-rw-r--r--declarations.mli6334logplain
-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.ml24757logplain
-rw-r--r--indtypes.mli1390logplain
-rw-r--r--inductive.ml34724logplain
-rw-r--r--inductive.mli4042logplain
-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.ml17992logplain
-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.ml17971logplain
-rw-r--r--reduction.mli3005logplain
-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