aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun444logplain
-rw-r--r--cClosure.ml37201logplain
-rw-r--r--cClosure.mli7927logplain
-rw-r--r--cPrimitives.ml2031logplain
-rw-r--r--cPrimitives.mli938logplain
-rw-r--r--cbytecodes.ml11023logplain
-rw-r--r--cbytecodes.mli7366logplain
-rw-r--r--cbytegen.ml42477logplain
-rw-r--r--cbytegen.mli1915logplain
-rw-r--r--cemitcodes.ml13440logplain
-rw-r--r--cemitcodes.mli988logplain
-rw-r--r--constr.ml38472logplain
-rw-r--r--constr.mli15239logplain
-rw-r--r--context.ml17121logplain
-rw-r--r--context.mli12024logplain
-rw-r--r--conv_oracle.ml3242logplain
-rw-r--r--conv_oracle.mli1697logplain
-rw-r--r--cooking.ml8343logplain
-rw-r--r--cooking.mli1161logplain
-rw-r--r--csymtable.ml7353logplain
-rw-r--r--csymtable.mli708logplain
-rw-r--r--declarations.ml11057logplain
-rw-r--r--declareops.ml12805logplain
-rw-r--r--declareops.mli2704logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml4368logplain
-rw-r--r--environ.ml22605logplain
-rw-r--r--environ.mli10407logplain
-rw-r--r--esubst.ml5783logplain
-rw-r--r--esubst.mli2865logplain
-rw-r--r--evar.ml690logplain
-rw-r--r--evar.mli1322logplain
-rw-r--r--indtypes.ml41554logplain
-rw-r--r--indtypes.mli1726logplain
-rw-r--r--inductive.ml46332logplain
-rw-r--r--inductive.mli5290logplain
-rw-r--r--kernel.mllib426logplain
-rw-r--r--make-opcodes170logplain
-rw-r--r--mod_subst.ml18051logplain
-rw-r--r--mod_subst.mli5921logplain
-rw-r--r--mod_typing.ml14609logplain
-rw-r--r--mod_typing.mli2235logplain
-rw-r--r--modops.ml22407logplain
-rw-r--r--modops.mli5045logplain
-rw-r--r--names.ml27237logplain
-rw-r--r--names.mli23339logplain
-rw-r--r--nativecode.ml73682logplain
-rw-r--r--nativecode.mli2319logplain
-rw-r--r--nativeconv.ml6752logplain
-rw-r--r--nativeconv.mli901logplain
-rw-r--r--nativeinstr.mli2212logplain
-rw-r--r--nativelambda.ml21655logplain
-rw-r--r--nativelambda.mli1551logplain
-rw-r--r--nativelib.ml5600logplain
-rw-r--r--nativelib.mli1230logplain
-rw-r--r--nativelibrary.ml2709logplain
-rw-r--r--nativelibrary.mli768logplain
-rw-r--r--nativevalues.ml15575logplain
-rw-r--r--nativevalues.mli4903logplain
-rw-r--r--opaqueproof.ml5995logplain
-rw-r--r--opaqueproof.mli3361logplain
-rw-r--r--pre_env.ml5740logplain
-rw-r--r--pre_env.mli3078logplain
-rw-r--r--reduction.ml36372logplain
-rw-r--r--reduction.mli5018logplain
-rw-r--r--retroknowledge.ml7475logplain
-rw-r--r--retroknowledge.mli6866logplain
-rw-r--r--safe_typing.ml34008logplain
-rw-r--r--safe_typing.mli7560logplain
-rw-r--r--sorts.ml2637logplain
-rw-r--r--sorts.mli1198logplain
-rw-r--r--subtyping.ml18034logplain
-rw-r--r--subtyping.mli648logplain
-rw-r--r--term.ml23269logplain
-rw-r--r--term.mli17099logplain
-rw-r--r--term_typing.ml24350logplain
-rw-r--r--term_typing.mli3042logplain
-rw-r--r--type_errors.ml4627logplain
-rw-r--r--type_errors.mli4217logplain
-rw-r--r--typeops.ml17114logplain
-rw-r--r--typeops.mli3521logplain
-rw-r--r--uGraph.ml28866logplain
-rw-r--r--uGraph.mli2369logplain
-rw-r--r--uint31.ml4093logplain
-rw-r--r--uint31.mli912logplain
-rw-r--r--univ.ml33722logplain
-rw-r--r--univ.mli15298logplain
-rw-r--r--vars.ml11105logplain
-rw-r--r--vars.mli6849logplain
-rw-r--r--vconv.ml7553logplain
-rw-r--r--vconv.mli981logplain
-rw-r--r--vm.ml22336logplain
-rw-r--r--vm.mli2353logplain