summaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
d---------byterun526logplain
-rw-r--r--cbytecodes.ml9894logplain
-rw-r--r--cbytecodes.mli6103logplain
-rw-r--r--cbytegen.ml33526logplain
-rw-r--r--cbytegen.mli1744logplain
-rw-r--r--cemitcodes.ml11975logplain
-rw-r--r--cemitcodes.mli1045logplain
-rw-r--r--closure.ml37154logplain
-rw-r--r--closure.mli7731logplain
-rw-r--r--constr.ml37768logplain
-rw-r--r--constr.mli11600logplain
-rw-r--r--context.ml4950logplain
-rw-r--r--context.mli4705logplain
-rw-r--r--conv_oracle.ml3094logplain
-rw-r--r--conv_oracle.mli1697logplain
-rw-r--r--cooking.ml8493logplain
-rw-r--r--cooking.mli1087logplain
-rw-r--r--csymtable.ml7379logplain
-rw-r--r--csymtable.mli708logplain
-rw-r--r--declarations.mli9324logplain
-rw-r--r--declareops.ml11407logplain
-rw-r--r--declareops.mli3286logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.mli3554logplain
-rw-r--r--environ.ml22565logplain
-rw-r--r--environ.mli10510logplain
-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.ml14375logplain
-rw-r--r--fast_typeops.mli1115logplain
-rw-r--r--indtypes.ml31214logplain
-rw-r--r--indtypes.mli1721logplain
-rw-r--r--inductive.ml45379logplain
-rw-r--r--inductive.mli5217logplain
-rw-r--r--kernel.mllib421logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml18020logplain
-rw-r--r--mod_subst.mli5833logplain
-rw-r--r--mod_typing.ml11954logplain
-rw-r--r--mod_typing.mli1713logplain
-rw-r--r--modops.ml21249logplain
-rw-r--r--modops.mli5037logplain
-rw-r--r--names.ml23766logplain
-rw-r--r--names.mli19998logplain
-rw-r--r--nativecode.ml73453logplain
-rw-r--r--nativecode.mli2284logplain
-rw-r--r--nativeconv.ml5496logplain
-rw-r--r--nativeconv.mli711logplain
-rw-r--r--nativeinstr.mli2211logplain
-rw-r--r--nativelambda.ml24499logplain
-rw-r--r--nativelambda.mli1569logplain
-rw-r--r--nativelib.ml4704logplain
-rw-r--r--nativelib.mli1214logplain
-rw-r--r--nativelibrary.ml2699logplain
-rw-r--r--nativelibrary.mli773logplain
-rw-r--r--nativevalues.ml15868logplain
-rw-r--r--nativevalues.mli4903logplain
-rw-r--r--opaqueproof.ml5201logplain
-rw-r--r--opaqueproof.mli3334logplain
-rw-r--r--pre_env.ml5030logplain
-rw-r--r--pre_env.mli2657logplain
-rw-r--r--primitives.ml2031logplain
-rw-r--r--primitives.mli938logplain
-rw-r--r--reduction.ml30342logplain
-rw-r--r--reduction.mli5057logplain
-rw-r--r--retroknowledge.ml7464logplain
-rw-r--r--retroknowledge.mli6866logplain
-rw-r--r--safe_typing.ml29821logplain
-rw-r--r--safe_typing.mli5547logplain
-rw-r--r--sorts.ml2595logplain
-rw-r--r--sorts.mli1198logplain
-rw-r--r--subtyping.ml19545logplain
-rw-r--r--subtyping.mli650logplain
-rw-r--r--term.ml22004logplain
-rw-r--r--term.mli16247logplain
-rw-r--r--term_typing.ml12081logplain
-rw-r--r--term_typing.mli1832logplain
-rw-r--r--type_errors.ml4234logplain
-rw-r--r--type_errors.mli3824logplain
-rw-r--r--typeops.ml17956logplain
-rw-r--r--typeops.mli4464logplain
-rw-r--r--uint31.ml4092logplain
-rw-r--r--uint31.mli912logplain
-rw-r--r--univ.ml61155logplain
-rw-r--r--univ.mli13798logplain
-rw-r--r--vars.ml10572logplain
-rw-r--r--vars.mli3796logplain
-rw-r--r--vconv.ml8787logplain
-rw-r--r--vconv.mli816logplain
-rw-r--r--vm.ml20163logplain
-rw-r--r--vm.mli2261logplain
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 17:09:17 +0000