summaryrefslogtreecommitdiff
path: root/kernel
ModeNameSize
-rw-r--r--closure.ml38098logplain
-rw-r--r--closure.mli6728logplain
-rw-r--r--conv_oracle.ml1608logplain
-rw-r--r--conv_oracle.mli1370logplain
-rw-r--r--cooking.ml5219logplain
-rw-r--r--cooking.mli1309logplain
-rw-r--r--declarations.ml6113logplain
-rw-r--r--declarations.mli4402logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3097logplain
-rw-r--r--entries.mli3098logplain
-rw-r--r--environ.ml8372logplain
-rw-r--r--environ.mli5930logplain
-rw-r--r--esubst.ml4987logplain
-rw-r--r--esubst.mli1775logplain
-rw-r--r--indtypes.ml20242logplain
-rw-r--r--indtypes.mli1617logplain
-rw-r--r--inductive.ml30003logplain
-rw-r--r--inductive.mli2805logplain
-rw-r--r--mod_typing.ml10369logplain
-rw-r--r--mod_typing.mli905logplain
-rw-r--r--modops.ml7698logplain
-rw-r--r--modops.mli2889logplain
-rw-r--r--names.ml9254logplain
-rw-r--r--names.mli5470logplain
-rw-r--r--reduction.ml14178logplain
-rw-r--r--reduction.mli2078logplain
-rw-r--r--safe_typing.ml17009logplain
-rw-r--r--safe_typing.mli3854logplain
-rw-r--r--sign.ml6363logplain
-rw-r--r--sign.mli3613logplain
-rw-r--r--subtyping.ml7649logplain
-rw-r--r--subtyping.mli735logplain
-rw-r--r--term.ml38322logplain
-rw-r--r--term.mli17794logplain
-rw-r--r--term_typing.ml3709logplain
-rw-r--r--term_typing.mli1095logplain
-rw-r--r--type_errors.ml3774logplain
-rw-r--r--type_errors.mli3498logplain
-rw-r--r--typeops.ml14680logplain
-rw-r--r--typeops.mli3040logplain
-rw-r--r--univ.ml14305logplain
-rw-r--r--univ.mli1808logplain