aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml49842logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13054logplain
-rw-r--r--egrammar.mli2108logplain
-rw-r--r--extend.ml1796logplain
-rw-r--r--extend.mli1722logplain
-rw-r--r--g_ascii_syntax.ml2690logplain
-rw-r--r--g_constr.ml411305logplain
-rw-r--r--g_decl_mode.ml47853logplain
-rw-r--r--g_intsyntax.ml9119logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml48349logplain
-rw-r--r--g_minicoq.ml45440logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_natsyntax.ml2379logplain
-rw-r--r--g_natsyntax.mli572logplain
-rw-r--r--g_prim.ml42430logplain
-rw-r--r--g_proofs.ml44950logplain
-rw-r--r--g_rsyntax.ml4184logplain
-rw-r--r--g_string_syntax.ml2109logplain
-rw-r--r--g_tactic.ml417037logplain
-rw-r--r--g_vernac.ml428448logplain
-rw-r--r--g_xml.ml410111logplain
-rw-r--r--g_zsyntax.ml6647logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--lexer.ml420529logplain
-rw-r--r--lexer.mli1506logplain
-rw-r--r--pcoq.ml422947logplain
-rw-r--r--pcoq.mli7720logplain
-rw-r--r--ppconstr.ml22514logplain
-rw-r--r--ppconstr.mli2670logplain
-rw-r--r--ppdecl_proof.ml6420logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml38671logplain
-rw-r--r--pptactic.mli3470logplain
-rw-r--r--ppvernac.ml33036logplain
-rw-r--r--ppvernac.mli795logplain
-rw-r--r--prettyp.ml25855logplain
-rw-r--r--prettyp.mli3462logplain
-rw-r--r--printer.ml15550logplain
-rw-r--r--printer.mli4484logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44315logplain
-rw-r--r--q_coqast.ml421670logplain
-rw-r--r--q_util.ml44936logplain
-rw-r--r--q_util.mli1152logplain
-rw-r--r--search.ml6898logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml47159logplain
-rw-r--r--tactic_printer.ml6985logplain
-rw-r--r--tactic_printer.mli962logplain
-rw-r--r--vernacextend.ml43916logplain