aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
-rw-r--r--closure.ml32437logplain
-rw-r--r--closure.mli6739logplain
-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.ml5962logplain
-rw-r--r--declarations.mli3981logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3034logplain
-rw-r--r--entries.mli3034logplain
-rw-r--r--environ.ml7798logplain
-rw-r--r--environ.mli5590logplain
-rw-r--r--esubst.ml4008logplain
-rw-r--r--esubst.mli1646logplain
-rw-r--r--indtypes.ml19737logplain
-rw-r--r--indtypes.mli1551logplain
-rw-r--r--inductive.ml29436logplain
-rw-r--r--inductive.mli2736logplain
-rw-r--r--mod_typing.ml9046logplain
-rw-r--r--mod_typing.mli836logplain
-rw-r--r--modops.ml6585logplain
-rw-r--r--modops.mli2655logplain
-rw-r--r--names.ml8612logplain
-rw-r--r--names.mli4958logplain
-rw-r--r--reduction.ml13367logplain
-rw-r--r--reduction.mli2007logplain
-rw-r--r--safe_typing.ml14522logplain
-rw-r--r--safe_typing.mli3555logplain
-rw-r--r--sign.ml6243logplain
-rw-r--r--sign.mli3460logplain
-rw-r--r--subtyping.ml7744logplain
-rw-r--r--subtyping.mli669logplain
-rw-r--r--term.ml39363logplain
-rw-r--r--term.mli17626logplain
-rw-r--r--term_typing.ml3487logplain
-rw-r--r--term_typing.mli1027logplain
-rw-r--r--type_errors.ml3678logplain
-rw-r--r--type_errors.mli3405logplain
-rw-r--r--typeops.ml14224logplain
-rw-r--r--typeops.mli2975logplain
-rw-r--r--univ.ml14243logplain
-rw-r--r--univ.mli1745logplain