aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--decl_kinds.mli1877logplain
-rw-r--r--evar_kinds.mli1107logplain
-rw-r--r--locus.mli2799logplain
-rw-r--r--misctypes.mli1952logplain
-rw-r--r--tacexpr.mli11677logplain
-rw-r--r--vernacexpr.mli12850logplain