aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.ml5857logplain
-rw-r--r--decl_kinds.ml2020logplain
-rw-r--r--evar_kinds.ml1374logplain
-rw-r--r--extend.ml3193logplain
-rw-r--r--genredexpr.ml1911logplain
-rw-r--r--glob_term.ml4736logplain
-rw-r--r--intf.mllib119logplain
-rw-r--r--locus.ml2946logplain
-rw-r--r--misctypes.ml4417logplain
-rw-r--r--notation_term.ml4465logplain
-rw-r--r--pattern.ml1737logplain
-rw-r--r--tactypes.ml1632logplain
-rw-r--r--vernacexpr.ml19106logplain