aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.mlp9480logplain
-rw-r--r--coqpp_ast.mli2055logplain
-rw-r--r--coqpp_lex.mll4834logplain
-rw-r--r--coqpp_main.ml11955logplain
-rw-r--r--coqpp_parse.mly5187logplain
-rw-r--r--q_util.mli1750logplain
-rw-r--r--q_util.mlp4664logplain
-rw-r--r--tacextend.mlp3352logplain
-rw-r--r--vernacextend.mlp8617logplain