aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--decl_kinds.mli1842logplain
-rw-r--r--vernacexpr.mli12857logplain