aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
d---------byterun526logplain
-rw-r--r--cbytecodes.ml8891logplain
-rw-r--r--cbytecodes.mli5435logplain
-rw-r--r--cbytegen.ml32790logplain
-rw-r--r--cbytegen.mli1713logplain
-rw-r--r--cemitcodes.ml11176logplain
-rw-r--r--cemitcodes.mli931logplain
-rw-r--r--closure.ml33432logplain
-rw-r--r--closure.mli6479logplain
-rw-r--r--conv_oracle.ml2314logplain
-rw-r--r--conv_oracle.mli1513logplain
-rw-r--r--cooking.ml3900logplain
-rw-r--r--cooking.mli1079logplain
-rw-r--r--csymtable.ml5219logplain
-rw-r--r--csymtable.mli170logplain
-rw-r--r--declarations.ml8901logplain
-rw-r--r--declarations.mli6403logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml2656logplain
-rw-r--r--entries.mli2673logplain
-rw-r--r--environ.ml22400logplain
-rw-r--r--environ.mli9510logplain
-rw-r--r--esubst.ml5581logplain
-rw-r--r--esubst.mli2705logplain
-rw-r--r--indtypes.ml24783logplain
-rw-r--r--indtypes.mli1390logplain
-rw-r--r--inductive.ml34685logplain
-rw-r--r--inductive.mli4170logplain
-rw-r--r--kernel.mllib278logplain
-rw-r--r--make-opcodes102logplain
-rw-r--r--mod_subst.ml13600logplain
-rw-r--r--mod_subst.mli3180logplain
-rw-r--r--mod_typing.ml14104logplain
-rw-r--r--mod_typing.mli1075logplain
-rw-r--r--modops.ml17970logplain
-rw-r--r--modops.mli3299logplain
-rw-r--r--names.ml8974logplain
-rw-r--r--names.mli5911logplain
-rw-r--r--pre_env.ml3714logplain
-rw-r--r--pre_env.mli2421logplain
-rw-r--r--reduction.ml18316logplain
-rw-r--r--reduction.mli3143logplain
-rw-r--r--retroknowledge.ml8222logplain
-rw-r--r--retroknowledge.mli5913logplain
-rw-r--r--safe_typing.ml25809logplain
-rw-r--r--safe_typing.mli4302logplain
-rw-r--r--sign.ml2534logplain
-rw-r--r--sign.mli2335logplain
-rw-r--r--subtyping.ml15587logplain
-rw-r--r--subtyping.mli676logplain
-rw-r--r--term.ml43172logplain
-rw-r--r--term.mli20985logplain
-rw-r--r--term_typing.ml4395logplain
-rw-r--r--term_typing.mli1336logplain
-rw-r--r--type_errors.ml3797logplain
-rw-r--r--type_errors.mli3542logplain
-rw-r--r--typeops.ml16345logplain
-rw-r--r--typeops.mli3543logplain
-rw-r--r--univ.ml19747logplain
-rw-r--r--univ.mli2836logplain
-rw-r--r--vconv.ml7692logplain
-rw-r--r--vconv.mli841logplain
-rw-r--r--vm.ml19281logplain
-rw-r--r--vm.mli2291logplain