summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml410713logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13292logplain
-rw-r--r--egrammar.mli2169logplain
-rw-r--r--extend.ml1843logplain
-rw-r--r--extend.mli1770logplain
-rw-r--r--g_ascii_syntax.ml2761logplain
-rw-r--r--g_constr.ml416264logplain
-rw-r--r--g_decl_mode.ml47958logplain
-rw-r--r--g_intsyntax.ml10416logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml48439logplain
-rw-r--r--g_minicoq.mli1053logplain
-rw-r--r--g_natsyntax.ml2430logplain
-rw-r--r--g_natsyntax.mli696logplain
-rw-r--r--g_prim.ml43036logplain
-rw-r--r--g_proofs.ml45527logplain
-rw-r--r--g_rsyntax.ml4249logplain
-rw-r--r--g_string_syntax.ml2180logplain
-rw-r--r--g_tactic.ml423998logplain
-rw-r--r--g_vernac.ml431933logplain
-rw-r--r--g_xml.ml410214logplain
-rw-r--r--g_zsyntax.ml6700logplain
-rw-r--r--g_zsyntax.mli623logplain
-rw-r--r--lexer.ml417451logplain
-rw-r--r--lexer.mli1553logplain
-rw-r--r--pcoq.ml425713logplain
-rw-r--r--pcoq.mli8682logplain
-rw-r--r--ppconstr.ml24108logplain
-rw-r--r--ppconstr.mli2792logplain
-rw-r--r--ppdecl_proof.ml6492logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml40000logplain
-rw-r--r--pptactic.mli3581logplain
-rw-r--r--ppvernac.ml36069logplain
-rw-r--r--ppvernac.mli845logplain
-rw-r--r--prettyp.ml27531logplain
-rw-r--r--prettyp.mli3716logplain
-rw-r--r--printer.ml17614logplain
-rw-r--r--printer.mli5002logplain
-rw-r--r--printmod.ml5831logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44418logplain
-rw-r--r--q_coqast.ml423166logplain
-rw-r--r--q_util.ml45238logplain
-rw-r--r--q_util.mli1354logplain
-rw-r--r--search.ml6809logplain
-rw-r--r--search.mli2182logplain
-rw-r--r--tacextend.ml47225logplain
-rw-r--r--tactic_printer.ml7180logplain
-rw-r--r--tactic_printer.mli1097logplain
-rw-r--r--vernacextend.ml44146logplain