aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml411079logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml11456logplain
-rw-r--r--egrammar.mli1937logplain
-rw-r--r--extend.ml1985logplain
-rw-r--r--extend.mli1986logplain
-rw-r--r--extrawit.ml2082logplain
-rw-r--r--extrawit.mli2246logplain
-rw-r--r--g_constr.ml416073logplain
-rw-r--r--g_decl_mode.ml47902logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml48391logplain
-rw-r--r--g_natsyntax.mli642logplain
-rw-r--r--g_prim.ml43222logplain
-rw-r--r--g_proofs.ml45775logplain
-rw-r--r--g_tactic.ml423987logplain
-rw-r--r--g_vernac.ml432862logplain
-rw-r--r--g_xml.ml410185logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--grammar.mllib660logplain
-rw-r--r--highparsing.mllib62logplain
-rw-r--r--lexer.ml419088logplain
-rw-r--r--lexer.mli1399logplain
-rw-r--r--parsing.mllib107logplain
-rw-r--r--pcoq.ml425246logplain
-rw-r--r--pcoq.mli10521logplain
-rw-r--r--ppconstr.ml24301logplain
-rw-r--r--ppconstr.mli3719logplain
-rw-r--r--ppdecl_proof.ml6438logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml39763logplain
-rw-r--r--pptactic.mli3530logplain
-rw-r--r--ppvernac.ml36723logplain
-rw-r--r--ppvernac.mli795logplain
-rw-r--r--prettyp.ml27583logplain
-rw-r--r--prettyp.mli3724logplain
-rw-r--r--printer.ml17360logplain
-rw-r--r--printer.mli4952logplain
-rw-r--r--printmod.ml5828logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44368logplain
-rw-r--r--q_coqast.ml423241logplain
-rw-r--r--q_util.ml43565logplain
-rw-r--r--q_util.mli1297logplain
-rw-r--r--tacextend.ml47390logplain
-rw-r--r--tactic_printer.ml7174logplain
-rw-r--r--tactic_printer.mli1042logplain
-rw-r--r--vernacextend.ml42964logplain