aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
ModeNameSize
-rw-r--r--closure.ml32344logplain
-rw-r--r--closure.mli6643logplain
-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.ml5926logplain
-rw-r--r--declarations.mli4279logplain
-rw-r--r--doc.tex277logplain
-rw-r--r--entries.ml3034logplain
-rw-r--r--entries.mli3034logplain
-rw-r--r--environ.ml7916logplain
-rw-r--r--environ.mli5656logplain
-rw-r--r--esubst.ml4008logplain
-rw-r--r--esubst.mli1646logplain
-rw-r--r--indtypes.ml19714logplain
-rw-r--r--indtypes.mli1551logplain
-rw-r--r--inductive.ml29905logplain
-rw-r--r--inductive.mli2736logplain
-rw-r--r--mod_typing.ml10055logplain
-rw-r--r--mod_typing.mli836logplain
-rw-r--r--modops.ml7497logplain
-rw-r--r--modops.mli2824logplain
-rw-r--r--names.ml9144logplain
-rw-r--r--names.mli5407logplain
-rw-r--r--reduction.ml13398logplain
-rw-r--r--reduction.mli2007logplain
-rw-r--r--safe_typing.ml14833logplain
-rw-r--r--safe_typing.mli3531logplain
-rw-r--r--sign.ml6243logplain
-rw-r--r--sign.mli3460logplain
-rw-r--r--subtyping.ml7584logplain
-rw-r--r--subtyping.mli669logplain
-rw-r--r--term.ml38084logplain
-rw-r--r--term.mli17134logplain
-rw-r--r--term_typing.ml3642logplain
-rw-r--r--term_typing.mli1027logplain
-rw-r--r--type_errors.ml3696logplain
-rw-r--r--type_errors.mli3419logplain
-rw-r--r--typeops.ml14382logplain
-rw-r--r--typeops.mli2975logplain
-rw-r--r--univ.ml14243logplain
-rw-r--r--univ.mli1745logplain