aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.mlp9480logplain
-rw-r--r--q_util.mli1750logplain
-rw-r--r--q_util.mlp4645logplain
-rw-r--r--tacextend.mlp6817logplain
-rw-r--r--vernacextend.mlp8176logplain