summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml411068logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12267logplain
-rw-r--r--egrammar.mli2096logplain
-rw-r--r--extend.ml2191logplain
-rw-r--r--extend.mli2191logplain
-rw-r--r--extrawit.ml2082logplain
-rw-r--r--extrawit.mli2246logplain
-rw-r--r--g_constr.ml415763logplain
-rw-r--r--g_decl_mode.ml47821logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml48404logplain
-rw-r--r--g_natsyntax.mli642logplain
-rw-r--r--g_prim.ml43286logplain
-rw-r--r--g_proofs.ml45774logplain
-rw-r--r--g_tactic.ml426076logplain
-rw-r--r--g_vernac.ml434516logplain
-rw-r--r--g_xml.ml410177logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--grammar.mllib690logplain
-rw-r--r--highparsing.mllib62logplain
-rw-r--r--lexer.ml419143logplain
-rw-r--r--lexer.mli1399logplain
-rw-r--r--parsing.mllib107logplain
-rw-r--r--pcoq.ml425283logplain
-rw-r--r--pcoq.mli10566logplain
-rw-r--r--ppconstr.ml24341logplain
-rw-r--r--ppconstr.mli3683logplain
-rw-r--r--ppdecl_proof.ml6380logplain
-rw-r--r--ppdecl_proof.mli76logplain
-rw-r--r--pptactic.ml40484logplain
-rw-r--r--pptactic.mli3680logplain
-rw-r--r--ppvernac.ml37612logplain
-rw-r--r--ppvernac.mli794logplain
-rw-r--r--prettyp.ml27370logplain
-rw-r--r--prettyp.mli3724logplain
-rw-r--r--printer.ml17899logplain
-rw-r--r--printer.mli5246logplain
-rw-r--r--printmod.ml5645logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44350logplain
-rw-r--r--q_coqast.ml423222logplain
-rw-r--r--q_util.ml43564logplain
-rw-r--r--q_util.mli1297logplain
-rw-r--r--tacextend.ml47385logplain
-rw-r--r--tactic_printer.ml7132logplain
-rw-r--r--tactic_printer.mli1042logplain
-rw-r--r--vernacextend.ml42963logplain