aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
ModeNameSize
-rw-r--r--argextend.mlp9480logplain
-rw-r--r--coqpp_ast.mli1753logplain
-rw-r--r--coqpp_lex.mll4707logplain
-rw-r--r--coqpp_main.ml10114logplain
-rw-r--r--coqpp_parse.mly3463logplain
-rw-r--r--q_util.mli1750logplain
-rw-r--r--q_util.mlp4664logplain
-rw-r--r--tacextend.mlp3539logplain
-rw-r--r--vernacextend.mlp8617logplain