aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun444logplain
-rw-r--r--cClosure.ml37598logplain
-rw-r--r--cClosure.mli7952logplain
-rw-r--r--cPrimitives.ml2031logplain
-rw-r--r--cPrimitives.mli938logplain
-rw-r--r--cbytecodes.ml11049logplain
-rw-r--r--cbytecodes.mli7367logplain
-rw-r--r--cbytegen.ml42476logplain
-rw-r--r--cbytegen.mli2445logplain
-rw-r--r--cemitcodes.ml13446logplain
-rw-r--r--cemitcodes.mli992logplain
-rw-r--r--constr.ml44020logplain
-rw-r--r--constr.mli18548logplain
-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.ml8321logplain
-rw-r--r--cooking.mli1153logplain
-rw-r--r--csymtable.ml7357logplain
-rw-r--r--csymtable.mli714logplain
-rw-r--r--declarations.ml11141logplain
-rw-r--r--declareops.ml12786logplain
-rw-r--r--declareops.mli2676logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml4569logplain
-rw-r--r--environ.ml22556logplain
-rw-r--r--environ.mli10389logplain
-rw-r--r--esubst.ml5783logplain
-rw-r--r--esubst.mli2865logplain
-rw-r--r--evar.ml727logplain
-rw-r--r--evar.mli1376logplain
-rw-r--r--indtypes.ml41579logplain
-rw-r--r--indtypes.mli1722logplain
-rw-r--r--inductive.ml46508logplain
-rw-r--r--inductive.mli5240logplain
-rw-r--r--kernel.mllib426logplain
-rw-r--r--make-opcodes170logplain
-rw-r--r--mod_subst.ml18153logplain
-rw-r--r--mod_subst.mli5818logplain
-rw-r--r--mod_typing.ml14559logplain
-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.mli23590logplain
-rw-r--r--nativecode.ml73698logplain
-rw-r--r--nativecode.mli2332logplain
-rw-r--r--nativeconv.ml6753logplain
-rw-r--r--nativeconv.mli903logplain
-rw-r--r--nativeinstr.mli2224logplain
-rw-r--r--nativelambda.ml21613logplain
-rw-r--r--nativelambda.mli1539logplain
-rw-r--r--nativelib.ml5941logplain
-rw-r--r--nativelib.mli1231logplain
-rw-r--r--nativelibrary.ml2715logplain
-rw-r--r--nativelibrary.mli767logplain
-rw-r--r--nativevalues.ml15598logplain
-rw-r--r--nativevalues.mli4907logplain
-rw-r--r--opaqueproof.ml5896logplain
-rw-r--r--opaqueproof.mli3313logplain
-rw-r--r--pre_env.ml5742logplain
-rw-r--r--pre_env.mli3068logplain
-rw-r--r--reduction.ml36935logplain
-rw-r--r--reduction.mli5034logplain
-rw-r--r--retroknowledge.ml7476logplain
-rw-r--r--retroknowledge.mli6858logplain
-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.ml18046logplain
-rw-r--r--subtyping.mli649logplain
-rw-r--r--term.ml19990logplain
-rw-r--r--term.mli22443logplain
-rw-r--r--term_typing.ml24562logplain
-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.ml33826logplain
-rw-r--r--univ.mli15545logplain
-rw-r--r--vars.ml11113logplain
-rw-r--r--vars.mli6837logplain
-rw-r--r--vconv.ml7592logplain
-rw-r--r--vconv.mli983logplain
-rw-r--r--vm.ml22344logplain
-rw-r--r--vm.mli2873logplain