aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun526logplain
-rw-r--r--cbytecodes.ml9656logplain
-rw-r--r--cbytecodes.mli6013logplain
-rw-r--r--cbytegen.ml32970logplain
-rw-r--r--cbytegen.mli1717logplain
-rw-r--r--cemitcodes.ml11881logplain
-rw-r--r--cemitcodes.mli933logplain
-rw-r--r--closure.ml33757logplain
-rw-r--r--closure.mli6336logplain
-rw-r--r--conv_oracle.ml2399logplain
-rw-r--r--conv_oracle.mli1500logplain
-rw-r--r--cooking.ml4169logplain
-rw-r--r--cooking.mli1077logplain
-rw-r--r--csymtable.ml5997logplain
-rw-r--r--csymtable.mli708logplain
-rw-r--r--declarations.ml9759logplain
-rw-r--r--declarations.mli6553logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2850logplain
-rw-r--r--entries.mli2806logplain
-rw-r--r--environ.ml22665logplain
-rw-r--r--environ.mli8742logplain
-rw-r--r--esubst.ml5665logplain
-rw-r--r--esubst.mli2803logplain
-rw-r--r--indtypes.ml24768logplain
-rw-r--r--indtypes.mli1427logplain
-rw-r--r--inductive.ml34790logplain
-rw-r--r--inductive.mli4007logplain
-rw-r--r--kernel.mllib278logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml20334logplain
-rw-r--r--mod_subst.mli4782logplain
-rw-r--r--mod_typing.ml17099logplain
-rw-r--r--mod_typing.mli1578logplain
-rw-r--r--modops.ml20806logplain
-rw-r--r--modops.mli3032logplain
-rw-r--r--names.ml12471logplain
-rw-r--r--names.mli7446logplain
-rw-r--r--pre_env.ml3781logplain
-rw-r--r--pre_env.mli2268logplain
-rw-r--r--reduction.ml18789logplain
-rw-r--r--reduction.mli3156logplain
-rw-r--r--retroknowledge.ml8489logplain
-rw-r--r--retroknowledge.mli5897logplain
-rw-r--r--safe_typing.ml26947logplain
-rw-r--r--safe_typing.mli4394logplain
-rw-r--r--sign.ml2880logplain
-rw-r--r--sign.mli2370logplain
-rw-r--r--subtyping.ml15381logplain
-rw-r--r--subtyping.mli650logplain
-rw-r--r--term.ml43946logplain
-rw-r--r--term.mli22100logplain
-rw-r--r--term_typing.ml4581logplain
-rw-r--r--term_typing.mli1330logplain
-rw-r--r--type_errors.ml3793logplain
-rw-r--r--type_errors.mli3537logplain
-rw-r--r--typeops.ml16333logplain
-rw-r--r--typeops.mli3618logplain
-rw-r--r--univ.ml19890logplain
-rw-r--r--univ.mli2869logplain
-rw-r--r--vconv.ml7714logplain
-rw-r--r--vconv.mli827logplain
-rw-r--r--vm.ml19338logplain
-rw-r--r--vm.mli2400logplain