aboutsummaryrefslogtreecommitdiff
path: root/grammar
ModeNameSize
-rw-r--r--argextend.mlp7903logplain
-rw-r--r--dune1171logplain
-rw-r--r--q_util.mli1871logplain
-rw-r--r--q_util.mlp5581logplain
-rw-r--r--tacextend.mlp2617logplain
-rw-r--r--vernacextend.mlp4299logplain