aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml412169logplain
-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.ml19064logplain
-rw-r--r--egrammar.mli2002logplain
-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.ml419818logplain
-rw-r--r--g_cases.ml42884logplain
-rw-r--r--g_constr.ml413675logplain
-rw-r--r--g_constrnew.ml411003logplain
-rw-r--r--g_ltac.ml47751logplain
-rw-r--r--g_ltacnew.ml46721logplain
-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.ml44976logplain
-rw-r--r--g_rsyntax.ml11199logplain
-rw-r--r--g_tactic.ml414422logplain
-rw-r--r--g_tacticnew.ml415313logplain
-rw-r--r--g_vernac.ml418141logplain
-rw-r--r--g_vernacnew.ml426747logplain
-rw-r--r--g_xml.ml47769logplain
-rw-r--r--g_zsyntax.ml12519logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--g_zsyntaxnew.mli572logplain
-rw-r--r--lexer.ml417663logplain
-rw-r--r--lexer.mli1464logplain
-rw-r--r--pcoq.ml427074logplain
-rw-r--r--pcoq.mli6438logplain
-rw-r--r--ppconstr.ml12344logplain
-rw-r--r--ppconstr.mli1445logplain
-rw-r--r--pptactic.ml29030logplain
-rw-r--r--pptactic.mli3122logplain
-rw-r--r--prettyp.ml20604logplain
-rw-r--r--prettyp.mli2454logplain
-rw-r--r--printer.ml15562logplain
-rw-r--r--printer.mli2445logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_coqast.ml425032logplain
-rw-r--r--q_util.ml42341logplain
-rw-r--r--q_util.mli1064logplain
-rw-r--r--search.ml6955logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml49419logplain
-rw-r--r--tactic_printer.ml4365logplain
-rw-r--r--tactic_printer.mli996logplain
-rw-r--r--termast.ml18561logplain
-rw-r--r--termast.mli2066logplain
-rw-r--r--vernacextend.ml45191logplain