aboutsummaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml411152logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12932logplain
-rw-r--r--egrammar.mli2121logplain
-rw-r--r--extend.ml1770logplain
-rw-r--r--extend.mli1800logplain
-rw-r--r--g_basevernac.ml420076logplain
-rw-r--r--g_cases.ml42884logplain
-rw-r--r--g_constr.ml413711logplain
-rw-r--r--g_constrnew.ml410795logplain
-rw-r--r--g_ltac.ml47795logplain
-rw-r--r--g_ltacnew.ml46853logplain
-rw-r--r--g_minicoq.ml45440logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_module.ml41319logplain
-rw-r--r--g_natsyntax.ml2999logplain
-rw-r--r--g_natsyntax.mli572logplain
-rw-r--r--g_natsyntaxnew.mli572logplain
-rw-r--r--g_prim.ml43679logplain
-rw-r--r--g_primnew.ml42285logplain
-rw-r--r--g_proofs.ml45437logplain
-rw-r--r--g_proofsnew.ml45065logplain
-rw-r--r--g_rsyntax.ml4066logplain
-rw-r--r--g_tactic.ml414428logplain
-rw-r--r--g_tacticnew.ml414956logplain
-rw-r--r--g_vernac.ml418192logplain
-rw-r--r--g_vernacnew.ml426610logplain
-rw-r--r--g_xml.ml47824logplain
-rw-r--r--g_zsyntax.ml7574logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--g_zsyntaxnew.mli572logplain
-rw-r--r--lexer.ml415985logplain
-rw-r--r--lexer.mli1506logplain
-rw-r--r--pcoq.ml422354logplain
-rw-r--r--pcoq.mli6036logplain
-rw-r--r--ppconstr.ml672logplain
-rw-r--r--ppconstr.mli540logplain
-rw-r--r--pptactic.ml11245logplain
-rw-r--r--pptactic.mli2901logplain
-rw-r--r--prettyp.ml20215logplain
-rw-r--r--prettyp.mli2454logplain
-rw-r--r--printer.ml11014logplain
-rw-r--r--printer.mli2546logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_coqast.ml420451logplain
-rw-r--r--q_util.ml43650logplain
-rw-r--r--q_util.mli1139logplain
-rw-r--r--search.ml6898logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml47034logplain
-rw-r--r--tactic_printer.ml4412logplain
-rw-r--r--tactic_printer.mli996logplain
-rw-r--r--vernacextend.ml43912logplain