aboutsummaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
-rw-r--r--.merlin.in109logplain
d---------byterun531logplain
-rw-r--r--cClosure.ml51464logplain
-rw-r--r--cClosure.mli8042logplain
-rw-r--r--cPrimitives.ml8255logplain
-rw-r--r--cPrimitives.mli2747logplain
-rw-r--r--cbytecodes.ml5312logplain
-rw-r--r--cbytecodes.mli3094logplain
-rw-r--r--cbytegen.ml33148logplain
-rw-r--r--cbytegen.mli1317logplain
-rw-r--r--cemitcodes.ml17255logplain
-rw-r--r--cemitcodes.mli1533logplain
-rw-r--r--clambda.ml26130logplain
-rw-r--r--clambda.mli1543logplain
-rw-r--r--constr.ml56964logplain
-rw-r--r--constr.mli25719logplain
-rw-r--r--context.ml18323logplain
-rw-r--r--context.mli13502logplain
-rw-r--r--conv_oracle.ml3918logplain
-rw-r--r--conv_oracle.mli1883logplain
-rw-r--r--cooking.ml14504logplain
-rw-r--r--cooking.mli1527logplain
-rw-r--r--csymtable.ml6656logplain
-rw-r--r--csymtable.mli923logplain
-rw-r--r--declarations.ml12266logplain
-rw-r--r--declareops.ml13545logplain
-rw-r--r--declareops.mli3306logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--dune688logplain
-rw-r--r--entries.ml4382logplain
-rw-r--r--environ.ml25830logplain
-rw-r--r--environ.mli14350logplain
-rw-r--r--esubst.ml6859logplain
-rw-r--r--esubst.mli3436logplain
-rw-r--r--evar.ml877logplain
-rw-r--r--evar.mli1526logplain
-rw-r--r--float64.ml5616logplain
-rw-r--r--float64.mli2509logplain
-rw-r--r--genOpcodeFiles.ml4875logplain
-rw-r--r--indTyping.ml16291logplain
-rw-r--r--indTyping.mli1868logplain
-rw-r--r--indtypes.ml25359logplain
-rw-r--r--indtypes.mli889logplain
-rw-r--r--inductive.ml51560logplain
-rw-r--r--inductive.mli5541logplain
-rw-r--r--inferCumulativity.ml8370logplain
-rw-r--r--inferCumulativity.mli1104logplain
-rw-r--r--kernel.mllib517logplain
-rw-r--r--mod_subst.ml18603logplain
-rw-r--r--mod_subst.mli5970logplain
-rw-r--r--mod_typing.ml14776logplain
-rw-r--r--mod_typing.mli2433logplain
-rw-r--r--modops.ml22372logplain
-rw-r--r--modops.mli5254logplain
-rw-r--r--names.ml30898logplain
-rw-r--r--names.mli19748logplain
-rw-r--r--nativecode.ml78155logplain
-rw-r--r--nativecode.mli2483logplain
-rw-r--r--nativeconv.ml7603logplain
-rw-r--r--nativeconv.mli1053logplain
-rw-r--r--nativelambda.ml22551logplain
-rw-r--r--nativelambda.mli2968logplain
-rw-r--r--nativelib.ml7203logplain
-rw-r--r--nativelib.mli1980logplain
-rw-r--r--nativelibrary.ml2912logplain
-rw-r--r--nativelibrary.mli930logplain
-rw-r--r--nativevalues.ml17641logplain
-rw-r--r--nativevalues.mli7793logplain
-rw-r--r--opaqueproof.ml5013logplain
-rw-r--r--opaqueproof.mli2692logplain
-rw-r--r--primred.ml11278logplain
-rw-r--r--primred.mli2130logplain
-rw-r--r--reduction.ml39603logplain
-rw-r--r--reduction.mli5530logplain
-rw-r--r--relevanceops.ml4823logplain
-rw-r--r--relevanceops.mli1414logplain
-rw-r--r--retroknowledge.ml2217logplain
-rw-r--r--retroknowledge.mli1785logplain
-rw-r--r--safe_typing.ml53896logplain
-rw-r--r--safe_typing.mli8023logplain
-rw-r--r--section.ml6596logplain
-rw-r--r--section.mli3698logplain
-rw-r--r--sorts.ml3897logplain
-rw-r--r--sorts.mli1709logplain
-rw-r--r--subtyping.ml14838logplain
-rw-r--r--subtyping.mli799logplain
-rw-r--r--term.ml13055logplain
-rw-r--r--term.mli8099logplain
-rw-r--r--term_typing.ml13846logplain
-rw-r--r--term_typing.mli2057logplain
-rw-r--r--transparentState.ml1216logplain
-rw-r--r--transparentState.mli1078logplain
-rw-r--r--type_errors.ml8294logplain
-rw-r--r--type_errors.mli5689logplain
-rw-r--r--typeops.ml25355logplain
-rw-r--r--typeops.mli4958logplain
-rw-r--r--uGraph.ml7679logplain
-rw-r--r--uGraph.mli3686logplain
-rw-r--r--uint63.mli2394logplain
-rw-r--r--uint63_31.ml7717logplain
-rw-r--r--uint63_63.ml6699logplain
-rw-r--r--univ.ml34355logplain
-rw-r--r--univ.mli14797logplain
-rw-r--r--vars.ml10244logplain
-rw-r--r--vars.mli6746logplain
-rw-r--r--vconv.ml7842logplain
-rw-r--r--vconv.mli1032logplain
-rw-r--r--vm.ml6126logplain
-rw-r--r--vm.mli1446logplain
-rw-r--r--vmvalues.ml24318logplain
-rw-r--r--vmvalues.mli5021logplain
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:09:38 +0000