aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.mli5761logplain
-rw-r--r--decl_kinds.mli1982logplain
-rw-r--r--evar_kinds.mli1374logplain
-rw-r--r--extend.mli3193logplain
-rw-r--r--genredexpr.mli1911logplain
-rw-r--r--glob_term.mli4194logplain
-rw-r--r--locus.mli2946logplain
-rw-r--r--misctypes.mli4053logplain
-rw-r--r--notation_term.mli4073logplain
-rw-r--r--pattern.mli3373logplain
-rw-r--r--tactypes.mli1632logplain
-rw-r--r--vernacexpr.mli19175logplain