aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml410967logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12258logplain
-rw-r--r--egrammar.mli2085logplain
-rw-r--r--extend.ml1412logplain
-rw-r--r--extend.mli1389logplain
-rw-r--r--extrawit.ml2068logplain
-rw-r--r--extrawit.mli2222logplain
-rw-r--r--g_constr.ml415543logplain
-rw-r--r--g_intsyntax.mli575logplain
-rw-r--r--g_ltac.ml48365logplain
-rw-r--r--g_natsyntax.mli617logplain
-rw-r--r--g_prim.ml43238logplain
-rw-r--r--g_proofs.ml45993logplain
-rw-r--r--g_tactic.ml425944logplain
-rw-r--r--g_vernac.ml434893logplain
-rw-r--r--g_xml.ml410135logplain
-rw-r--r--g_zsyntax.mli547logplain
-rw-r--r--grammar.mllib700logplain
-rw-r--r--highparsing.mllib50logplain
-rw-r--r--lexer.ml419077logplain
-rw-r--r--lexer.mli1203logplain
-rw-r--r--parsing.mllib94logplain
-rw-r--r--pcoq.ml425783logplain
-rw-r--r--pcoq.mli10112logplain
-rw-r--r--ppconstr.ml21613logplain
-rw-r--r--ppconstr.mli3515logplain
-rw-r--r--pptactic.ml40465logplain
-rw-r--r--pptactic.mli3656logplain
-rw-r--r--ppvernac.ml37901logplain
-rw-r--r--ppvernac.mli768logplain
-rw-r--r--prettyp.ml27505logplain
-rw-r--r--prettyp.mli3692logplain
-rw-r--r--printer.ml17626logplain
-rw-r--r--printer.mli4956logplain
-rw-r--r--printmod.ml5645logplain
-rw-r--r--printmod.mli738logplain
-rw-r--r--q_constr.ml44334logplain
-rw-r--r--q_coqast.ml424189logplain
-rw-r--r--q_util.ml42611logplain
-rw-r--r--q_util.mli1224logplain
-rw-r--r--tacextend.ml47251logplain
-rw-r--r--tactic_printer.ml5375logplain
-rw-r--r--tactic_printer.mli945logplain
-rw-r--r--tok.ml2922logplain
-rw-r--r--tok.mli1014logplain
-rw-r--r--vernacextend.ml43368logplain