aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.ml411319logplain
-rw-r--r--grammar.mllib405logplain
-rw-r--r--q_constr.ml44452logplain
-rw-r--r--q_coqast.ml424612logplain
-rw-r--r--q_util.ml42720logplain
-rw-r--r--q_util.mli1263logplain
-rw-r--r--tacextend.ml49972logplain
-rw-r--r--vernacextend.ml46574logplain