aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun444logplain
-rw-r--r--cClosure.ml37404logplain
-rw-r--r--cClosure.mli8138logplain
-rw-r--r--cPrimitives.ml2031logplain
-rw-r--r--cPrimitives.mli938logplain
-rw-r--r--cbytecodes.ml12084logplain
-rw-r--r--cbytecodes.mli7058logplain
-rw-r--r--cbytegen.ml34110logplain
-rw-r--r--cbytegen.mli1032logplain
-rw-r--r--cemitcodes.ml15506logplain
-rw-r--r--cemitcodes.mli803logplain
-rw-r--r--cinstr.mli1716logplain
-rw-r--r--clambda.ml27246logplain
-rw-r--r--clambda.mli1128logplain
-rw-r--r--constr.ml43925logplain
-rw-r--r--constr.mli18493logplain
-rw-r--r--context.ml17115logplain
-rw-r--r--context.mli12024logplain
-rw-r--r--conv_oracle.ml3242logplain
-rw-r--r--conv_oracle.mli1705logplain
-rw-r--r--cooking.ml8757logplain
-rw-r--r--cooking.mli1153logplain
-rw-r--r--csymtable.ml5275logplain
-rw-r--r--csymtable.mli723logplain
-rw-r--r--declarations.ml11223logplain
-rw-r--r--declareops.ml12817logplain
-rw-r--r--declareops.mli2698logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml4569logplain
-rw-r--r--environ.ml22050logplain
-rw-r--r--environ.mli10215logplain
-rw-r--r--esubst.ml5783logplain
-rw-r--r--esubst.mli2865logplain
-rw-r--r--evar.ml727logplain
-rw-r--r--evar.mli1376logplain
-rw-r--r--indtypes.ml42088logplain
-rw-r--r--indtypes.mli1722logplain
-rw-r--r--inductive.ml46568logplain
-rw-r--r--inductive.mli5240logplain
-rw-r--r--kernel.mllib443logplain
-rw-r--r--make-opcodes170logplain
-rw-r--r--mod_subst.ml18153logplain
-rw-r--r--mod_subst.mli5818logplain
-rw-r--r--mod_typing.ml14129logplain
-rw-r--r--mod_typing.mli2223logplain
-rw-r--r--modops.ml22420logplain
-rw-r--r--modops.mli5021logplain
-rw-r--r--names.ml27238logplain
-rw-r--r--names.mli23309logplain
-rw-r--r--nativecode.ml73730logplain
-rw-r--r--nativecode.mli2327logplain
-rw-r--r--nativeconv.ml6983logplain
-rw-r--r--nativeconv.mli903logplain
-rw-r--r--nativeinstr.mli2250logplain
-rw-r--r--nativelambda.ml22098logplain
-rw-r--r--nativelambda.mli1539logplain
-rw-r--r--nativelib.ml5852logplain
-rw-r--r--nativelib.mli1231logplain
-rw-r--r--nativelibrary.ml2715logplain
-rw-r--r--nativelibrary.mli767logplain
-rw-r--r--nativevalues.ml15587logplain
-rw-r--r--nativevalues.mli4946logplain
-rw-r--r--opaqueproof.ml5885logplain
-rw-r--r--opaqueproof.mli3302logplain
-rw-r--r--pre_env.ml6379logplain
-rw-r--r--pre_env.mli3449logplain
-rw-r--r--reduction.ml35633logplain
-rw-r--r--reduction.mli5472logplain
-rw-r--r--retroknowledge.ml7328logplain
-rw-r--r--retroknowledge.mli6441logplain
-rw-r--r--safe_typing.ml33374logplain
-rw-r--r--safe_typing.mli7608logplain
-rw-r--r--sorts.ml2643logplain
-rw-r--r--sorts.mli1204logplain
-rw-r--r--subtyping.ml18544logplain
-rw-r--r--subtyping.mli649logplain
-rw-r--r--term.ml20100logplain
-rw-r--r--term.mli22439logplain
-rw-r--r--term_typing.ml25155logplain
-rw-r--r--term_typing.mli2880logplain
-rw-r--r--type_errors.ml4644logplain
-rw-r--r--type_errors.mli4209logplain
-rw-r--r--typeops.ml17132logplain
-rw-r--r--typeops.mli3748logplain
-rw-r--r--uGraph.ml28875logplain
-rw-r--r--uGraph.mli2346logplain
-rw-r--r--uint31.ml4093logplain
-rw-r--r--uint31.mli912logplain
-rw-r--r--univ.ml34265logplain
-rw-r--r--univ.mli16393logplain
-rw-r--r--vars.ml9851logplain
-rw-r--r--vars.mli6616logplain
-rw-r--r--vconv.ml7566logplain
-rw-r--r--vconv.mli992logplain
-rw-r--r--vm.ml5691logplain
-rw-r--r--vm.mli1296logplain
-rw-r--r--vmvalues.ml18169logplain
-rw-r--r--vmvalues.mli3427logplain