aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
-rw-r--r--closure.ml34194logplain
-rw-r--r--closure.mli7238logplain
-rw-r--r--cooking.ml4629logplain
-rw-r--r--cooking.mli1233logplain
-rw-r--r--declarations.ml2094logplain
-rw-r--r--declarations.mli2094logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--environ.ml9636logplain
-rw-r--r--environ.mli4549logplain
-rw-r--r--esubst.ml4008logplain
-rw-r--r--esubst.mli1646logplain
-rw-r--r--indtypes.ml19185logplain
-rw-r--r--indtypes.mli2410logplain
-rw-r--r--inductive.ml28814logplain
-rw-r--r--inductive.mli2697logplain
-rw-r--r--names.ml4826logplain
-rw-r--r--names.mli2735logplain
-rw-r--r--reduction.ml10465logplain
-rw-r--r--reduction.mli1784logplain
-rw-r--r--safe_typing.ml4422logplain
-rw-r--r--safe_typing.mli2705logplain
-rw-r--r--sign.ml7458logplain
-rw-r--r--sign.mli3333logplain
-rw-r--r--term.ml41172logplain
-rw-r--r--term.mli17135logplain
-rw-r--r--type_errors.ml3474logplain
-rw-r--r--type_errors.mli3248logplain
-rw-r--r--typeops.ml14197logplain
-rw-r--r--typeops.mli2945logplain
-rw-r--r--univ.ml14668logplain
-rw-r--r--univ.mli1747logplain