aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml47800logplain
-rwxr-xr-xast.ml25060logplain
-rwxr-xr-xast.mli4556logplain
-rw-r--r--astmod.ml4587logplain
-rw-r--r--astmod.mli979logplain
-rw-r--r--astterm.ml30634logplain
-rw-r--r--astterm.mli3814logplain
-rw-r--r--coqast.ml8754logplain
-rw-r--r--coqast.mli1638logplain
-rw-r--r--coqlib.ml10141logplain
-rw-r--r--coqlib.mli3649logplain
-rw-r--r--egrammar.ml9702logplain
-rw-r--r--egrammar.mli1392logplain
-rw-r--r--esyntax.ml8895logplain
-rw-r--r--esyntax.mli1638logplain
-rw-r--r--extend.ml8527logplain
-rw-r--r--extend.mli3612logplain
-rw-r--r--g_basevernac.ml412486logplain
-rw-r--r--g_cases.ml42175logplain
-rw-r--r--g_constr.ml49955logplain
-rw-r--r--g_ltac.ml49016logplain
-rw-r--r--g_minicoq.ml45476logplain
-rw-r--r--g_minicoq.mli995logplain
-rw-r--r--g_module.ml42007logplain
-rw-r--r--g_natsyntax.ml2797logplain
-rw-r--r--g_natsyntax.mli565logplain
-rw-r--r--g_prim.ml45044logplain
-rw-r--r--g_proofs.ml45057logplain
-rw-r--r--g_rsyntax.ml2414logplain
-rw-r--r--g_tactic.ml412956logplain
-rw-r--r--g_vernac.ml415743logplain
-rw-r--r--g_zsyntax.ml5110logplain
-rw-r--r--g_zsyntax.mli625logplain
-rw-r--r--genarg.ml4926logplain
-rw-r--r--genarg.mli8040logplain
-rw-r--r--lexer.ml49363logplain
-rw-r--r--lexer.mli1093logplain
-rw-r--r--pcoq.ml416986logplain
-rw-r--r--pcoq.mli6140logplain
-rw-r--r--ppconstr.ml5018logplain
-rw-r--r--ppconstr.mli1333logplain
-rw-r--r--pptactic.ml22012logplain
-rw-r--r--pptactic.mli1486logplain
-rw-r--r--pretty.ml18986logplain
-rw-r--r--prettyp.ml19028logplain
-rw-r--r--prettyp.mli2230logplain
-rw-r--r--printer.ml6805logplain
-rw-r--r--printer.mli2377logplain
-rw-r--r--q_coqast.ml421512logplain
-rw-r--r--q_util.ml42256logplain
-rw-r--r--q_util.mli1016logplain
-rw-r--r--search.ml6097logplain
-rw-r--r--search.mli1628logplain
-rw-r--r--tacextend.ml47342logplain
-rw-r--r--termast.ml13826logplain
-rw-r--r--termast.mli1882logplain
-rw-r--r--vernacextend.ml46115logplain