aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.ml413877logplain
-rw-r--r--grammar.mllib310logplain
-rw-r--r--q_constr.ml44408logplain
-rw-r--r--q_coqast.ml425758logplain
-rw-r--r--q_util.ml42710logplain
-rw-r--r--q_util.mli1236logplain
-rw-r--r--tacextend.ml48462logplain
-rw-r--r--vernacextend.ml43521logplain