aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml411068logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12305logplain
-rw-r--r--egrammar.mli2110logplain
-rw-r--r--extend.ml2191logplain
-rw-r--r--extend.mli2172logplain
-rw-r--r--extrawit.ml2082logplain
-rw-r--r--extrawit.mli2236logplain
-rw-r--r--g_constr.ml415763logplain
-rw-r--r--g_intsyntax.mli575logplain
-rw-r--r--g_ltac.ml48404logplain
-rw-r--r--g_natsyntax.mli631logplain
-rw-r--r--g_prim.ml43286logplain
-rw-r--r--g_proofs.ml46019logplain
-rw-r--r--g_tactic.ml426076logplain
-rw-r--r--g_vernac.ml434859logplain
-rw-r--r--g_xml.ml410177logplain
-rw-r--r--g_zsyntax.mli561logplain
-rw-r--r--grammar.mllib696logplain
-rw-r--r--highparsing.mllib50logplain
-rw-r--r--lexer.ml419026logplain
-rw-r--r--lexer.mli1389logplain
-rw-r--r--parsing.mllib94logplain
-rw-r--r--pcoq.ml425224logplain
-rw-r--r--pcoq.mli10499logplain
-rw-r--r--ppconstr.ml24316logplain
-rw-r--r--ppconstr.mli3635logplain
-rw-r--r--pptactic.ml40477logplain
-rw-r--r--pptactic.mli3670logplain
-rw-r--r--ppvernac.ml37921logplain
-rw-r--r--ppvernac.mli782logplain
-rw-r--r--prettyp.ml27517logplain
-rw-r--r--prettyp.mli3706logplain
-rw-r--r--printer.ml17638logplain
-rw-r--r--printer.mli4970logplain
-rw-r--r--printmod.ml5645logplain
-rw-r--r--printmod.mli738logplain
-rw-r--r--q_constr.ml44350logplain
-rw-r--r--q_coqast.ml423222logplain
-rw-r--r--q_util.ml43564logplain
-rw-r--r--q_util.mli1285logplain
-rw-r--r--tacextend.ml47385logplain
-rw-r--r--tactic_printer.ml5387logplain
-rw-r--r--tactic_printer.mli959logplain
-rw-r--r--vernacextend.ml43554logplain