aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.ml411775logplain
-rw-r--r--grammar.mllib460logplain
-rw-r--r--q_constr.ml44475logplain
-rw-r--r--q_coqast.ml424658logplain
-rw-r--r--q_util.ml43650logplain
-rw-r--r--q_util.mli1270logplain
-rw-r--r--tacextend.ml410139logplain
-rw-r--r--vernacextend.ml47369logplain