aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.mlp9239logplain
-rw-r--r--compat5.ml685logplain
-rw-r--r--compat5.mlp965logplain
-rw-r--r--compat5b.mlp977logplain
-rw-r--r--gramCompat.mlp2114logplain
-rw-r--r--q_util.mli1569logplain
-rw-r--r--q_util.mlp4177logplain
-rw-r--r--tacextend.mlp6402logplain
-rw-r--r--vernacextend.mlp7008logplain