aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.mli5894logplain
-rw-r--r--decl_kinds.mli1983logplain
-rw-r--r--evar_kinds.mli1203logplain
-rw-r--r--extend.mli3196logplain
-rw-r--r--genredexpr.mli1650logplain
-rw-r--r--glob_term.mli3870logplain
-rw-r--r--locus.mli2946logplain
-rw-r--r--misctypes.mli3172logplain
-rw-r--r--notation_term.mli3502logplain
-rw-r--r--pattern.mli3333logplain
-rw-r--r--tacexpr.mli11846logplain
-rw-r--r--vernacexpr.mli16943logplain