aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
-rw-r--r--.cvsignore12logplain
d---------byterun440logplain
-rw-r--r--cbytecodes.ml3906logplain
-rw-r--r--cbytecodes.mli1710logplain
-rw-r--r--cbytegen.ml15606logplain
-rw-r--r--cbytegen.mli352logplain
-rw-r--r--cemitcodes.ml9031logplain
-rw-r--r--cemitcodes.mli939logplain
-rw-r--r--closure.ml37737logplain
-rw-r--r--closure.mli6641logplain
-rw-r--r--conv_oracle.ml1570logplain
-rw-r--r--conv_oracle.mli1301logplain
-rw-r--r--cooking.ml3584logplain
-rw-r--r--cooking.mli1064logplain
-rw-r--r--csymtable.ml4939logplain
-rw-r--r--csymtable.mli171logplain
-rw-r--r--declarations.ml6464logplain
-rw-r--r--declarations.mli4770logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3107logplain
-rw-r--r--entries.mli3107logplain
-rw-r--r--environ.ml10170logplain
-rw-r--r--environ.mli8099logplain
-rw-r--r--esubst.ml4932logplain
-rw-r--r--esubst.mli1719logplain
-rw-r--r--indtypes.ml21643logplain
-rw-r--r--indtypes.mli1343logplain
-rw-r--r--inductive.ml30375logplain
-rw-r--r--inductive.mli2748logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml7546logplain
-rw-r--r--mod_subst.mli2745logplain
-rw-r--r--mod_typing.ml12035logplain
-rw-r--r--mod_typing.mli926logplain
-rw-r--r--modops.ml10207logplain
-rw-r--r--modops.mli3001logplain
-rw-r--r--names.ml8436logplain
-rw-r--r--names.mli5209logplain
-rw-r--r--pre_env.ml3772logplain
-rw-r--r--pre_env.mli2311logplain
-rw-r--r--reduction.ml14820logplain
-rw-r--r--reduction.mli2520logplain
-rw-r--r--safe_typing.ml16901logplain
-rw-r--r--safe_typing.mli3821logplain
-rw-r--r--sign.ml6349logplain
-rw-r--r--sign.mli3675logplain
-rw-r--r--subtyping.ml9432logplain
-rw-r--r--subtyping.mli676logplain
-rw-r--r--term.ml38214logplain
-rw-r--r--term.mli18069logplain
-rw-r--r--term_typing.ml3668logplain
-rw-r--r--term_typing.mli1059logplain
-rw-r--r--type_errors.ml3723logplain
-rw-r--r--type_errors.mli3446logplain
-rw-r--r--typeops.ml14903logplain
-rw-r--r--typeops.mli2995logplain
-rw-r--r--univ.ml14537logplain
-rw-r--r--univ.mli1711logplain
-rw-r--r--vconv.ml18057logplain
-rw-r--r--vconv.mli1372logplain
-rw-r--r--vm.ml15808logplain
-rw-r--r--vm.mli2510logplain