summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml411120logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12822logplain
-rw-r--r--egrammar.mli2511logplain
-rw-r--r--extend.ml2306logplain
-rw-r--r--extend.mli2307logplain
-rw-r--r--extrawit.ml2132logplain
-rw-r--r--extrawit.mli2297logplain
-rw-r--r--g_constr.ml415906logplain
-rw-r--r--g_decl_mode.ml47875logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml48453logplain
-rw-r--r--g_natsyntax.mli696logplain
-rw-r--r--g_prim.ml43335logplain
-rw-r--r--g_proofs.ml45825logplain
-rw-r--r--g_tactic.ml426127logplain
-rw-r--r--g_vernac.ml434842logplain
-rw-r--r--g_xml.ml410225logplain
-rw-r--r--g_zsyntax.mli624logplain
-rw-r--r--grammar.mllib690logplain
-rw-r--r--highparsing.mllib62logplain
-rw-r--r--lexer.ml419203logplain
-rw-r--r--lexer.mli1447logplain
-rw-r--r--parsing.mllib107logplain
-rw-r--r--pcoq.ml426137logplain
-rw-r--r--pcoq.mli10705logplain
-rw-r--r--ppconstr.ml24649logplain
-rw-r--r--ppconstr.mli3733logplain
-rw-r--r--ppdecl_proof.ml6434logplain
-rw-r--r--ppdecl_proof.mli76logplain
-rw-r--r--pptactic.ml40534logplain
-rw-r--r--pptactic.mli3731logplain
-rw-r--r--ppvernac.ml38100logplain
-rw-r--r--ppvernac.mli845logplain
-rw-r--r--prettyp.ml28887logplain
-rw-r--r--prettyp.mli3566logplain
-rw-r--r--printer.ml17970logplain
-rw-r--r--printer.mli5296logplain
-rw-r--r--printmod.ml5645logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44401logplain
-rw-r--r--q_coqast.ml423264logplain
-rw-r--r--q_util.ml43613logplain
-rw-r--r--q_util.mli1346logplain
-rw-r--r--tacextend.ml47437logplain
-rw-r--r--tactic_printer.ml7188logplain
-rw-r--r--tactic_printer.mli1099logplain
-rw-r--r--vernacextend.ml43018logplain