aboutsummaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
d---------byterun444logplain
-rw-r--r--cClosure.ml38377logplain
-rw-r--r--cClosure.mli8393logplain
-rw-r--r--cPrimitives.ml2181logplain
-rw-r--r--cPrimitives.mli1088logplain
-rw-r--r--cbytecodes.ml12267logplain
-rw-r--r--cbytecodes.mli7175logplain
-rw-r--r--cbytegen.ml35360logplain
-rw-r--r--cbytegen.mli1280logplain
-rw-r--r--cemitcodes.ml15941logplain
-rw-r--r--cemitcodes.mli844logplain
-rw-r--r--cinstr.mli2146logplain
-rw-r--r--clambda.ml27555logplain
-rw-r--r--clambda.mli1227logplain
-rw-r--r--constr.ml45937logplain
-rw-r--r--constr.mli20001logplain
-rw-r--r--context.ml17380logplain
-rw-r--r--context.mli12423logplain
-rw-r--r--conv_oracle.ml3392logplain
-rw-r--r--conv_oracle.mli1855logplain
-rw-r--r--cooking.ml7910logplain
-rw-r--r--cooking.mli1250logplain
-rw-r--r--csymtable.ml6133logplain
-rw-r--r--csymtable.mli923logplain
-rw-r--r--declarations.ml11316logplain
-rw-r--r--declareops.ml13375logplain
-rw-r--r--declareops.mli3090logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml4663logplain
-rw-r--r--environ.ml21922logplain
-rw-r--r--environ.mli11991logplain
-rw-r--r--esubst.ml6859logplain
-rw-r--r--esubst.mli3437logplain
-rw-r--r--evar.ml877logplain
-rw-r--r--evar.mli1526logplain
-rw-r--r--indtypes.ml40103logplain
-rw-r--r--indtypes.mli1680logplain
-rw-r--r--inductive.ml46649logplain
-rw-r--r--inductive.mli5410logplain
-rw-r--r--kernel.mllib435logplain
-rw-r--r--make-opcodes170logplain
-rw-r--r--mod_subst.ml18579logplain
-rw-r--r--mod_subst.mli6129logplain
-rw-r--r--mod_typing.ml14309logplain
-rw-r--r--mod_typing.mli2373logplain
-rw-r--r--modops.ml22634logplain
-rw-r--r--modops.mli5134logplain
-rw-r--r--names.ml28930logplain
-rw-r--r--names.mli18310logplain
-rw-r--r--nativecode.ml75562logplain
-rw-r--r--nativecode.mli2517logplain
-rw-r--r--nativeconv.ml7141logplain
-rw-r--r--nativeconv.mli1053logplain
-rw-r--r--nativeinstr.mli2685logplain
-rw-r--r--nativelambda.ml21943logplain
-rw-r--r--nativelambda.mli1696logplain
-rw-r--r--nativelib.ml6050logplain
-rw-r--r--nativelib.mli1381logplain
-rw-r--r--nativelibrary.ml2835logplain
-rw-r--r--nativelibrary.mli917logplain
-rw-r--r--nativevalues.ml15603logplain
-rw-r--r--nativevalues.mli5079logplain
-rw-r--r--opaqueproof.ml6040logplain
-rw-r--r--opaqueproof.mli3457logplain
-rw-r--r--reduction.ml35300logplain
-rw-r--r--reduction.mli5589logplain
-rw-r--r--retroknowledge.ml7197logplain
-rw-r--r--retroknowledge.mli6373logplain
-rw-r--r--safe_typing.ml39746logplain
-rw-r--r--safe_typing.mli7815logplain
-rw-r--r--sorts.ml2600logplain
-rw-r--r--sorts.mli1287logplain
-rw-r--r--subtyping.ml15140logplain
-rw-r--r--subtyping.mli799logplain
-rw-r--r--term.ml13545logplain
-rw-r--r--term.mli8061logplain
-rw-r--r--term_typing.ml23455logplain
-rw-r--r--term_typing.mli3030logplain
-rw-r--r--type_errors.ml4794logplain
-rw-r--r--type_errors.mli4359logplain
-rw-r--r--typeops.ml16806logplain
-rw-r--r--typeops.mli3761logplain
-rw-r--r--uGraph.ml31605logplain
-rw-r--r--uGraph.mli3146logplain
-rw-r--r--uint31.ml4093logplain
-rw-r--r--uint31.mli912logplain
-rw-r--r--univ.ml34038logplain
-rw-r--r--univ.mli16748logplain
-rw-r--r--vars.ml9908logplain
-rw-r--r--vars.mli6702logplain
-rw-r--r--vconv.ml7859logplain
-rw-r--r--vconv.mli1032logplain
-rw-r--r--vm.ml5976logplain
-rw-r--r--vm.mli1446logplain
-rw-r--r--vmvalues.ml19090logplain
-rw-r--r--vmvalues.mli3953logplain
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:25:13 +0000