aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.ml6100logplain
-rw-r--r--decl_kinds.ml2503logplain
-rw-r--r--evar_kinds.ml1576logplain
-rw-r--r--extend.ml5010logplain
-rw-r--r--genredexpr.ml2049logplain
-rw-r--r--glob_term.ml5391logplain
-rw-r--r--intf.mllib110logplain
-rw-r--r--locus.ml3096logplain
-rw-r--r--misctypes.ml4838logplain
-rw-r--r--notation_term.ml5108logplain
-rw-r--r--pattern.ml1898logplain
-rw-r--r--vernacexpr.ml19995logplain