aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml411152logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12942logplain
-rw-r--r--egrammar.mli2121logplain
-rw-r--r--extend.ml1796logplain
-rw-r--r--extend.mli1722logplain
-rw-r--r--g_ascii_syntax.ml2690logplain
-rw-r--r--g_constr.ml411082logplain
-rw-r--r--g_ltac.ml47105logplain
-rw-r--r--g_minicoq.ml45440logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_natsyntax.ml2283logplain
-rw-r--r--g_natsyntax.mli572logplain
-rw-r--r--g_natsyntaxnew.mli572logplain
-rw-r--r--g_prim.ml42430logplain
-rw-r--r--g_proofs.ml44868logplain
-rw-r--r--g_rsyntax.ml4184logplain
-rw-r--r--g_string_syntax.ml2109logplain
-rw-r--r--g_tactic.ml416053logplain
-rw-r--r--g_vernac.ml427025logplain
-rw-r--r--g_xml.ml48581logplain
-rw-r--r--g_zsyntax.ml6647logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--g_zsyntaxnew.mli572logplain
-rw-r--r--lexer.ml416636logplain
-rw-r--r--lexer.mli1506logplain
-rw-r--r--pcoq.ml420777logplain
-rw-r--r--pcoq.mli5982logplain
-rw-r--r--ppconstr.ml21843logplain
-rw-r--r--ppconstr.mli2231logplain
-rw-r--r--pptactic.ml36826logplain
-rw-r--r--pptactic.mli3302logplain
-rw-r--r--ppvernac.ml31663logplain
-rw-r--r--ppvernac.mli795logplain
-rw-r--r--prettyp.ml19321logplain
-rw-r--r--prettyp.mli2409logplain
-rw-r--r--printer.ml11718logplain
-rw-r--r--printer.mli3429logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44308logplain
-rw-r--r--q_coqast.ml421062logplain
-rw-r--r--q_util.ml43650logplain
-rw-r--r--q_util.mli1139logplain
-rw-r--r--search.ml6902logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml47034logplain
-rw-r--r--tactic_printer.ml4410logplain
-rw-r--r--tactic_printer.mli996logplain
-rw-r--r--vernacextend.ml43912logplain