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_constr.ml410911logplain
-rw-r--r--g_ltac.ml46853logplain
-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.ml42334logplain
-rw-r--r--g_proofs.ml45062logplain
-rw-r--r--g_rsyntax.ml4065logplain
-rw-r--r--g_tactic.ml414956logplain
-rw-r--r--g_vernac.ml426604logplain
-rw-r--r--g_xml.ml47824logplain
-rw-r--r--g_zsyntax.ml6485logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--g_zsyntaxnew.mli572logplain
-rw-r--r--lexer.ml415947logplain
-rw-r--r--lexer.mli1506logplain
-rw-r--r--pcoq.ml420967logplain
-rw-r--r--pcoq.mli6036logplain
-rw-r--r--ppconstr.ml23574logplain
-rw-r--r--ppconstr.mli3054logplain
-rw-r--r--pptactic.ml36507logplain
-rw-r--r--pptactic.mli3231logplain
-rw-r--r--ppvernac.ml32026logplain
-rw-r--r--ppvernac.mli795logplain
-rw-r--r--prettyp.ml19149logplain
-rw-r--r--prettyp.mli2409logplain
-rw-r--r--printer.ml10944logplain
-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.ml4406logplain
-rw-r--r--tactic_printer.mli996logplain
-rw-r--r--vernacextend.ml43912logplain