aboutsummaryrefslogtreecommitdiff
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.mli4684logplain
-rw-r--r--decl_kinds.mli1877logplain
-rw-r--r--evar_kinds.mli1107logplain
-rw-r--r--genredexpr.mli1514logplain
-rw-r--r--glob_term.mli2942logplain
-rw-r--r--locus.mli2799logplain
-rw-r--r--misctypes.mli2136logplain
-rw-r--r--notation_term.mli3269logplain
-rw-r--r--tacexpr.mli11302logplain
-rw-r--r--vernacexpr.mli12870logplain