aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.mli5277logplain
-rw-r--r--decl_kinds.mli1889logplain
-rw-r--r--evar_kinds.mli1098logplain
-rw-r--r--extend.mli1590logplain
-rw-r--r--genredexpr.mli1585logplain
-rw-r--r--glob_term.mli3022logplain
-rw-r--r--locus.mli2775logplain
-rw-r--r--misctypes.mli2407logplain
-rw-r--r--notation_term.mli3236logplain
-rw-r--r--pattern.mli3288logplain
-rw-r--r--tacexpr.mli10294logplain
-rw-r--r--vernacexpr.mli13135logplain