aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml411008logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12293logplain
-rw-r--r--egrammar.mli2096logplain
-rw-r--r--extend.ml2177logplain
-rw-r--r--extend.mli2158logplain
-rw-r--r--extrawit.ml2068logplain
-rw-r--r--extrawit.mli2222logplain
-rw-r--r--g_constr.ml415715logplain
-rw-r--r--g_intsyntax.mli575logplain
-rw-r--r--g_ltac.ml48356logplain
-rw-r--r--g_natsyntax.mli617logplain
-rw-r--r--g_prim.ml43236logplain
-rw-r--r--g_proofs.ml45970logplain
-rw-r--r--g_tactic.ml426028logplain
-rw-r--r--g_vernac.ml434861logplain
-rw-r--r--g_xml.ml410129logplain
-rw-r--r--g_zsyntax.mli547logplain
-rw-r--r--grammar.mllib696logplain
-rw-r--r--highparsing.mllib50logplain
-rw-r--r--lexer.ml418987logplain
-rw-r--r--lexer.mli1375logplain
-rw-r--r--parsing.mllib94logplain
-rw-r--r--pcoq.ml425123logplain
-rw-r--r--pcoq.mli10485logplain
-rw-r--r--ppconstr.ml21613logplain
-rw-r--r--ppconstr.mli3515logplain
-rw-r--r--pptactic.ml40465logplain
-rw-r--r--pptactic.mli3656logplain
-rw-r--r--ppvernac.ml37963logplain
-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.ml44290logplain
-rw-r--r--q_coqast.ml422960logplain
-rw-r--r--q_util.ml43518logplain
-rw-r--r--q_util.mli1271logplain
-rw-r--r--tacextend.ml47325logplain
-rw-r--r--tactic_printer.ml5375logplain
-rw-r--r--tactic_printer.mli945logplain
-rw-r--r--vernacextend.ml43494logplain