aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun526logplain
-rw-r--r--cbytecodes.ml9656logplain
-rw-r--r--cbytecodes.mli6013logplain
-rw-r--r--cbytegen.ml32856logplain
-rw-r--r--cbytegen.mli1742logplain
-rw-r--r--cemitcodes.ml11849logplain
-rw-r--r--cemitcodes.mli1013logplain
-rw-r--r--closure.ml33621logplain
-rw-r--r--closure.mli6409logplain
-rw-r--r--conv_oracle.ml2417logplain
-rw-r--r--conv_oracle.mli1508logplain
-rw-r--r--cooking.ml4524logplain
-rw-r--r--cooking.mli1065logplain
-rw-r--r--csymtable.ml6453logplain
-rw-r--r--csymtable.mli708logplain
-rw-r--r--declarations.ml13141logplain
-rw-r--r--declarations.mli8102logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2760logplain
-rw-r--r--entries.mli2738logplain
-rw-r--r--environ.ml17257logplain
-rw-r--r--environ.mli7932logplain
-rw-r--r--esubst.ml5719logplain
-rw-r--r--esubst.mli2865logplain
-rw-r--r--indtypes.ml25256logplain
-rw-r--r--indtypes.mli1427logplain
-rw-r--r--inductive.ml34817logplain
-rw-r--r--inductive.mli4451logplain
-rw-r--r--kernel.mllib279logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml17334logplain
-rw-r--r--mod_subst.mli5105logplain
-rw-r--r--mod_typing.ml15298logplain
-rw-r--r--mod_typing.mli1722logplain
-rw-r--r--modops.ml20655logplain
-rw-r--r--modops.mli4009logplain
-rw-r--r--names.ml14565logplain
-rw-r--r--names.mli7871logplain
-rw-r--r--pre_env.ml3793logplain
-rw-r--r--pre_env.mli2258logplain
-rw-r--r--reduction.ml20052logplain
-rw-r--r--reduction.mli3344logplain
-rw-r--r--retroknowledge.ml8490logplain
-rw-r--r--retroknowledge.mli5897logplain
-rw-r--r--safe_typing.ml28262logplain
-rw-r--r--safe_typing.mli4678logplain
-rw-r--r--sign.ml2950logplain
-rw-r--r--sign.mli2466logplain
-rw-r--r--subtyping.ml16342logplain
-rw-r--r--subtyping.mli650logplain
-rw-r--r--term.ml49169logplain
-rw-r--r--term.mli22405logplain
-rw-r--r--term_typing.ml5382logplain
-rw-r--r--term_typing.mli1318logplain
-rw-r--r--type_errors.ml4011logplain
-rw-r--r--type_errors.mli3622logplain
-rw-r--r--typeops.ml16420logplain
-rw-r--r--typeops.mli3692logplain
-rw-r--r--univ.ml30856logplain
-rw-r--r--univ.mli3744logplain
-rw-r--r--vconv.ml7880logplain
-rw-r--r--vconv.mli827logplain
-rw-r--r--vm.ml20136logplain
-rw-r--r--vm.mli2435logplain