aboutsummaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
-rw-r--r--.merlin.in109logplain
d---------byterun526logplain
-rw-r--r--cClosure.ml47049logplain
-rw-r--r--cClosure.mli7929logplain
-rw-r--r--cPrimitives.ml3858logplain
-rw-r--r--cPrimitives.mli1679logplain
-rw-r--r--cbytecodes.ml5200logplain
-rw-r--r--cbytecodes.mli3059logplain
-rw-r--r--cbytegen.ml32847logplain
-rw-r--r--cbytegen.mli1310logplain
-rw-r--r--cemitcodes.ml16485logplain
-rw-r--r--cemitcodes.mli1533logplain
-rw-r--r--clambda.ml25979logplain
-rw-r--r--clambda.mli1512logplain
-rw-r--r--constr.ml55371logplain
-rw-r--r--constr.mli25563logplain
-rw-r--r--context.ml18458logplain
-rw-r--r--context.mli13498logplain
-rw-r--r--conv_oracle.ml3773logplain
-rw-r--r--conv_oracle.mli1856logplain
-rw-r--r--cooking.ml13277logplain
-rw-r--r--cooking.mli1542logplain
-rw-r--r--csymtable.ml6136logplain
-rw-r--r--csymtable.mli923logplain
-rw-r--r--declarations.ml12190logplain
-rw-r--r--declareops.ml13517logplain
-rw-r--r--declareops.mli3306logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--dune688logplain
-rw-r--r--entries.ml4642logplain
-rw-r--r--environ.ml25784logplain
-rw-r--r--environ.mli13921logplain
-rw-r--r--esubst.ml6859logplain
-rw-r--r--esubst.mli3437logplain
-rw-r--r--evar.ml877logplain
-rw-r--r--evar.mli1526logplain
-rw-r--r--genOpcodeFiles.ml4433logplain
-rw-r--r--indTyping.ml16300logplain
-rw-r--r--indTyping.mli1710logplain
-rw-r--r--indtypes.ml24088logplain
-rw-r--r--indtypes.mli848logplain
-rw-r--r--inductive.ml49581logplain
-rw-r--r--inductive.mli5505logplain
-rw-r--r--inferCumulativity.ml8935logplain
-rw-r--r--inferCumulativity.mli851logplain
-rw-r--r--kernel.mllib506logplain
-rw-r--r--mod_subst.ml18080logplain
-rw-r--r--mod_subst.mli5970logplain
-rw-r--r--mod_typing.ml14885logplain
-rw-r--r--mod_typing.mli2373logplain
-rw-r--r--modops.ml21991logplain
-rw-r--r--modops.mli5254logplain
-rw-r--r--names.ml30687logplain
-rw-r--r--names.mli19423logplain
-rw-r--r--nativecode.ml75423logplain
-rw-r--r--nativecode.mli2483logplain
-rw-r--r--nativeconv.ml7143logplain
-rw-r--r--nativeconv.mli1053logplain
-rw-r--r--nativelambda.ml22049logplain
-rw-r--r--nativelambda.mli2937logplain
-rw-r--r--nativelib.ml6240logplain
-rw-r--r--nativelib.mli1915logplain
-rw-r--r--nativelibrary.ml2828logplain
-rw-r--r--nativelibrary.mli930logplain
-rw-r--r--nativevalues.ml13664logplain
-rw-r--r--nativevalues.mli6049logplain
-rw-r--r--opaqueproof.ml5950logplain
-rw-r--r--opaqueproof.mli3120logplain
-rw-r--r--primred.ml6542logplain
-rw-r--r--primred.mli1248logplain
-rw-r--r--reduction.ml38925logplain
-rw-r--r--reduction.mli5533logplain
-rw-r--r--retroknowledge.ml1576logplain
-rw-r--r--retroknowledge.mli1218logplain
-rw-r--r--retypeops.ml4917logplain
-rw-r--r--retypeops.mli1441logplain
-rw-r--r--safe_typing.ml51146logplain
-rw-r--r--safe_typing.mli7669logplain
-rw-r--r--section.ml7478logplain
-rw-r--r--section.mli3367logplain
-rw-r--r--sorts.ml3832logplain
-rw-r--r--sorts.mli1677logplain
-rw-r--r--subtyping.ml14594logplain
-rw-r--r--subtyping.mli799logplain
-rw-r--r--term.ml13811logplain
-rw-r--r--term.mli8461logplain
-rw-r--r--term_typing.ml14091logplain
-rw-r--r--term_typing.mli1952logplain
-rw-r--r--transparentState.ml1216logplain
-rw-r--r--transparentState.mli1078logplain
-rw-r--r--type_errors.ml8251logplain
-rw-r--r--type_errors.mli5584logplain
-rw-r--r--typeops.ml24474logplain
-rw-r--r--typeops.mli4878logplain
-rw-r--r--uGraph.ml7522logplain
-rw-r--r--uGraph.mli3585logplain
-rw-r--r--uint63.mli2186logplain
-rw-r--r--uint63_31.ml7253logplain
-rw-r--r--uint63_63.ml6486logplain
-rw-r--r--univ.ml33640logplain
-rw-r--r--univ.mli14631logplain
-rw-r--r--vars.ml10243logplain
-rw-r--r--vars.mli6890logplain
-rw-r--r--vconv.ml7586logplain
-rw-r--r--vconv.mli1032logplain
-rw-r--r--vm.ml5971logplain
-rw-r--r--vm.mli1446logplain
-rw-r--r--vmvalues.ml23662logplain
-rw-r--r--vmvalues.mli4970logplain
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:24:34 +0000