aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
-rw-r--r--closure.ml38032logplain
-rw-r--r--closure.mli6659logplain
-rw-r--r--conv_oracle.ml1653logplain
-rw-r--r--conv_oracle.mli1229logplain
-rw-r--r--cooking.ml5155logplain
-rw-r--r--cooking.mli1245logplain
-rw-r--r--declarations.ml6044logplain
-rw-r--r--declarations.mli4320logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3034logplain
-rw-r--r--entries.mli3034logplain
-rw-r--r--environ.ml8308logplain
-rw-r--r--environ.mli5855logplain
-rw-r--r--esubst.ml4925logplain
-rw-r--r--esubst.mli1710logplain
-rw-r--r--indtypes.ml20168logplain
-rw-r--r--indtypes.mli1551logplain
-rw-r--r--inductive.ml29922logplain
-rw-r--r--inductive.mli2736logplain
-rw-r--r--mod_typing.ml10302logplain
-rw-r--r--mod_typing.mli836logplain
-rw-r--r--modops.ml7635logplain
-rw-r--r--modops.mli2824logplain
-rw-r--r--names.ml9144logplain
-rw-r--r--names.mli5407logplain
-rw-r--r--reduction.ml14112logplain
-rw-r--r--reduction.mli2007logplain
-rw-r--r--safe_typing.ml16941logplain
-rw-r--r--safe_typing.mli3785logplain
-rw-r--r--sign.ml6302logplain
-rw-r--r--sign.mli3551logplain
-rw-r--r--subtyping.ml7583logplain
-rw-r--r--subtyping.mli669logplain
-rw-r--r--term.ml38259logplain
-rw-r--r--term.mli17731logplain
-rw-r--r--term_typing.ml3642logplain
-rw-r--r--term_typing.mli1027logplain
-rw-r--r--type_errors.ml3706logplain
-rw-r--r--type_errors.mli3429logplain
-rw-r--r--typeops.ml14614logplain
-rw-r--r--typeops.mli2975logplain
-rw-r--r--univ.ml14243logplain
-rw-r--r--univ.mli1745logplain