aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
-rw-r--r--closure.ml32171logplain
-rw-r--r--closure.mli6588logplain
-rw-r--r--conv_oracle.ml1653logplain
-rw-r--r--conv_oracle.mli1229logplain
-rw-r--r--cooking.ml4648logplain
-rw-r--r--cooking.mli1233logplain
-rw-r--r--declarations.ml2094logplain
-rw-r--r--declarations.mli2094logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--environ.ml9846logplain
-rw-r--r--environ.mli4566logplain
-rw-r--r--esubst.ml4008logplain
-rw-r--r--esubst.mli1646logplain
-rw-r--r--indtypes.ml18577logplain
-rw-r--r--indtypes.mli2410logplain
-rw-r--r--inductive.ml31689logplain
-rw-r--r--inductive.mli2712logplain
-rw-r--r--names.ml4296logplain
-rw-r--r--names.mli2660logplain
-rw-r--r--reduction.ml13152logplain
-rw-r--r--reduction.mli1912logplain
-rw-r--r--safe_typing.ml4148logplain
-rw-r--r--safe_typing.mli2613logplain
-rw-r--r--sign.ml6151logplain
-rw-r--r--sign.mli3503logplain
-rw-r--r--term.ml38638logplain
-rw-r--r--term.mli17320logplain
-rw-r--r--type_errors.ml3678logplain
-rw-r--r--type_errors.mli3405logplain
-rw-r--r--typeops.ml14140logplain
-rw-r--r--typeops.mli2938logplain
-rw-r--r--univ.ml14156logplain
-rw-r--r--univ.mli1745logplain