aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.ml48431logplain
-rw-r--r--grammar.mllib83logplain
-rw-r--r--q_constr.ml44475logplain
-rw-r--r--q_util.ml44175logplain
-rw-r--r--q_util.mli1305logplain
-rw-r--r--tacextend.ml46488logplain
-rw-r--r--vernacextend.ml46878logplain