aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
ModeNameSize
-rw-r--r--constrexpr.ml5749logplain
-rw-r--r--decl_kinds.ml2353logplain
-rw-r--r--evar_kinds.ml1358logplain
-rw-r--r--extend.ml4239logplain
-rw-r--r--genredexpr.ml1899logplain
-rw-r--r--glob_term.ml5256logplain
-rw-r--r--intf.mllib110logplain
-rw-r--r--locus.ml2946logplain
-rw-r--r--misctypes.ml4675logplain
-rw-r--r--notation_term.ml4958logplain
-rw-r--r--pattern.ml1748logplain
-rw-r--r--vernacexpr.ml19790logplain