summaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
d---------byterun526logplain
-rw-r--r--cbytecodes.ml8891logplain
-rw-r--r--cbytecodes.mli5435logplain
-rw-r--r--cbytegen.ml32804logplain
-rw-r--r--cbytegen.mli1713logplain
-rw-r--r--cemitcodes.ml11241logplain
-rw-r--r--cemitcodes.mli1061logplain
-rw-r--r--closure.ml33395logplain
-rw-r--r--closure.mli6378logplain
-rw-r--r--conv_oracle.ml2367logplain
-rw-r--r--conv_oracle.mli1567logplain
-rw-r--r--cooking.ml3967logplain
-rw-r--r--cooking.mli1131logplain
-rw-r--r--csymtable.ml5793logplain
-rw-r--r--csymtable.mli170logplain
-rw-r--r--declarations.ml8843logplain
-rw-r--r--declarations.mli6852logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2913logplain
-rw-r--r--entries.mli2891logplain
-rw-r--r--environ.ml16718logplain
-rw-r--r--environ.mli8597logplain
-rw-r--r--esubst.ml5629logplain
-rw-r--r--esubst.mli2754logplain
-rw-r--r--indtypes.ml25581logplain
-rw-r--r--indtypes.mli1441logplain
-rw-r--r--inductive.ml35954logplain
-rw-r--r--inductive.mli4722logplain
-rw-r--r--kernel.mllib279logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml20291logplain
-rw-r--r--mod_subst.mli5062logplain
-rw-r--r--mod_typing.ml16975logplain
-rw-r--r--mod_typing.mli1657logplain
-rw-r--r--modops.ml19568logplain
-rw-r--r--modops.mli3105logplain
-rw-r--r--names.ml12041logplain
-rw-r--r--names.mli7555logplain
-rw-r--r--pre_env.ml3602logplain
-rw-r--r--pre_env.mli2323logplain
-rw-r--r--reduction.ml18684logplain
-rw-r--r--reduction.mli3236logplain
-rw-r--r--retroknowledge.ml8279logplain
-rw-r--r--retroknowledge.mli5970logplain
-rw-r--r--safe_typing.ml25460logplain
-rw-r--r--safe_typing.mli4439logplain
-rw-r--r--sign.ml2580logplain
-rw-r--r--sign.mli2382logplain
-rw-r--r--subtyping.ml15313logplain
-rw-r--r--subtyping.mli728logplain
-rw-r--r--term.ml43257logplain
-rw-r--r--term.mli21042logplain
-rw-r--r--term_typing.ml4448logplain
-rw-r--r--term_typing.mli1390logplain
-rw-r--r--type_errors.ml3850logplain
-rw-r--r--type_errors.mli3596logplain
-rw-r--r--typeops.ml16394logplain
-rw-r--r--typeops.mli3593logplain
-rw-r--r--univ.ml19855logplain
-rw-r--r--univ.mli2883logplain
-rw-r--r--vconv.ml7714logplain
-rw-r--r--vconv.mli841logplain
-rw-r--r--vm.ml18972logplain
-rw-r--r--vm.mli2360logplain