aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml412200logplain
-rwxr-xr-xast.ml18529logplain
-rwxr-xr-xast.mli3437logplain
-rw-r--r--coqast.ml3661logplain
-rw-r--r--coqast.mli1645logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml20528logplain
-rw-r--r--egrammar.mli1874logplain
-rw-r--r--esyntax.ml9511logplain
-rw-r--r--esyntax.mli1608logplain
-rw-r--r--extend.ml11817logplain
-rw-r--r--extend.mli4273logplain
-rw-r--r--g_basevernac.ml420079logplain
-rw-r--r--g_cases.ml42884logplain
-rw-r--r--g_constr.ml413675logplain
-rw-r--r--g_constrnew.ml411048logplain
-rw-r--r--g_ltac.ml47795logplain
-rw-r--r--g_ltacnew.ml46905logplain
-rw-r--r--g_minicoq.ml45440logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_module.ml41319logplain
-rw-r--r--g_natsyntax.ml6022logplain
-rw-r--r--g_natsyntax.mli572logplain
-rw-r--r--g_natsyntaxnew.mli572logplain
-rw-r--r--g_prim.ml44201logplain
-rw-r--r--g_primnew.ml42589logplain
-rw-r--r--g_proofs.ml45437logplain
-rw-r--r--g_proofsnew.ml45056logplain
-rw-r--r--g_rsyntax.ml11199logplain
-rw-r--r--g_tactic.ml414428logplain
-rw-r--r--g_tacticnew.ml415319logplain
-rw-r--r--g_vernac.ml418141logplain
-rw-r--r--g_vernacnew.ml426991logplain
-rw-r--r--g_xml.ml47769logplain
-rw-r--r--g_zsyntax.ml12467logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--g_zsyntaxnew.mli572logplain
-rw-r--r--lexer.ml417636logplain
-rw-r--r--lexer.mli1464logplain
-rw-r--r--pcoq.ml427567logplain
-rw-r--r--pcoq.mli6922logplain
-rw-r--r--ppconstr.ml12344logplain
-rw-r--r--ppconstr.mli1445logplain
-rw-r--r--pptactic.ml29901logplain
-rw-r--r--pptactic.mli3286logplain
-rw-r--r--prettyp.ml20499logplain
-rw-r--r--prettyp.mli2454logplain
-rw-r--r--printer.ml15789logplain
-rw-r--r--printer.mli2546logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_coqast.ml425071logplain
-rw-r--r--q_util.ml42341logplain
-rw-r--r--q_util.mli1064logplain
-rw-r--r--search.ml6908logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml49208logplain
-rw-r--r--tactic_printer.ml4312logplain
-rw-r--r--tactic_printer.mli996logplain
-rw-r--r--termast.ml18476logplain
-rw-r--r--termast.mli2066logplain
-rw-r--r--vernacextend.ml45165logplain