aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun444logplain
-rw-r--r--cClosure.ml36770logplain
-rw-r--r--cClosure.mli7929logplain
-rw-r--r--cbytecodes.ml11033logplain
-rw-r--r--cbytecodes.mli7393logplain
-rw-r--r--cbytegen.ml42448logplain
-rw-r--r--cbytegen.mli1922logplain
-rw-r--r--cemitcodes.ml12652logplain
-rw-r--r--cemitcodes.mli988logplain
-rw-r--r--constr.ml38482logplain
-rw-r--r--constr.mli15066logplain
-rw-r--r--context.ml16720logplain
-rw-r--r--context.mli10714logplain
-rw-r--r--conv_oracle.ml3230logplain
-rw-r--r--conv_oracle.mli1697logplain
-rw-r--r--cooking.ml8617logplain
-rw-r--r--cooking.mli1079logplain
-rw-r--r--csymtable.ml7353logplain
-rw-r--r--csymtable.mli708logplain
-rw-r--r--declarations.mli10756logplain
-rw-r--r--declareops.ml13471logplain
-rw-r--r--declareops.mli2895logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.mli4052logplain
-rw-r--r--environ.ml22718logplain
-rw-r--r--environ.mli10522logplain
-rw-r--r--esubst.ml5783logplain
-rw-r--r--esubst.mli2865logplain
-rw-r--r--evar.ml690logplain
-rw-r--r--evar.mli1322logplain
-rw-r--r--fast_typeops.ml14569logplain
-rw-r--r--fast_typeops.mli1068logplain
-rw-r--r--indtypes.ml38141logplain
-rw-r--r--indtypes.mli1726logplain
-rw-r--r--inductive.ml46087logplain
-rw-r--r--inductive.mli5290logplain
-rw-r--r--kernel.mllib417logplain
-rw-r--r--make-opcodes170logplain
-rw-r--r--mod_subst.ml18051logplain
-rw-r--r--mod_subst.mli5939logplain
-rw-r--r--mod_typing.ml14815logplain
-rw-r--r--mod_typing.mli2235logplain
-rw-r--r--modops.ml21911logplain
-rw-r--r--modops.mli5008logplain
-rw-r--r--names.ml27587logplain
-rw-r--r--names.mli23311logplain
-rw-r--r--nativecode.ml74119logplain
-rw-r--r--nativecode.mli2319logplain
-rw-r--r--nativeconv.ml6735logplain
-rw-r--r--nativeconv.mli901logplain
-rw-r--r--nativeinstr.mli2211logplain
-rw-r--r--nativelambda.ml24621logplain
-rw-r--r--nativelambda.mli1550logplain
-rw-r--r--nativelib.ml5396logplain
-rw-r--r--nativelib.mli1214logplain
-rw-r--r--nativelibrary.ml2709logplain
-rw-r--r--nativelibrary.mli768logplain
-rw-r--r--nativevalues.ml15503logplain
-rw-r--r--nativevalues.mli4903logplain
-rw-r--r--opaqueproof.ml5321logplain
-rw-r--r--opaqueproof.mli3319logplain
-rw-r--r--pre_env.ml6068logplain
-rw-r--r--pre_env.mli3078logplain
-rw-r--r--primitives.ml2031logplain
-rw-r--r--primitives.mli938logplain
-rw-r--r--reduction.ml28448logplain
-rw-r--r--reduction.mli4423logplain
-rw-r--r--retroknowledge.ml7464logplain
-rw-r--r--retroknowledge.mli6866logplain
-rw-r--r--safe_typing.ml32832logplain
-rw-r--r--safe_typing.mli7000logplain
-rw-r--r--sorts.ml2637logplain
-rw-r--r--sorts.mli1198logplain
-rw-r--r--subtyping.ml19746logplain
-rw-r--r--subtyping.mli650logplain
-rw-r--r--term.ml23175logplain
-rw-r--r--term.mli17015logplain
-rw-r--r--term_typing.ml20299logplain
-rw-r--r--term_typing.mli2696logplain
-rw-r--r--type_errors.ml4627logplain
-rw-r--r--type_errors.mli4217logplain
-rw-r--r--typeops.ml18454logplain
-rw-r--r--typeops.mli4453logplain
-rw-r--r--uGraph.ml28684logplain
-rw-r--r--uGraph.mli2125logplain
-rw-r--r--uint31.ml4093logplain
-rw-r--r--uint31.mli912logplain
-rw-r--r--univ.ml33055logplain
-rw-r--r--univ.mli12860logplain
-rw-r--r--vars.ml10868logplain
-rw-r--r--vars.mli6622logplain
-rw-r--r--vconv.ml7279logplain
-rw-r--r--vconv.mli981logplain
-rw-r--r--vm.ml22313logplain
-rw-r--r--vm.mli2380logplain