aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.mlp9342logplain
-rw-r--r--compat5.ml685logplain
-rw-r--r--q_util.mli1593logplain
-rw-r--r--q_util.mlp4228logplain
-rw-r--r--tacextend.mlp6686logplain
-rw-r--r--vernacextend.mlp6953logplain