aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.ml49279logplain
-rw-r--r--gramCompat.ml42114logplain
-rw-r--r--grammar.mllib51logplain
-rw-r--r--q_constr.ml44301logplain
-rw-r--r--q_util.ml44177logplain
-rw-r--r--q_util.mli1569logplain
-rw-r--r--tacextend.ml46845logplain
-rw-r--r--vernacextend.ml47232logplain