aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml412115logplain
-rwxr-xr-xast.ml18778logplain
-rwxr-xr-xast.mli3507logplain
-rw-r--r--coqast.ml4067logplain
-rw-r--r--coqast.mli1633logplain
-rw-r--r--egrammar.ml18775logplain
-rw-r--r--egrammar.mli1812logplain
-rw-r--r--esyntax.ml9488logplain
-rw-r--r--esyntax.mli1851logplain
-rw-r--r--extend.ml11817logplain
-rw-r--r--extend.mli4432logplain
-rw-r--r--g_basevernac.ml419607logplain
-rw-r--r--g_cases.ml42640logplain
-rw-r--r--g_constr.ml413430logplain
-rw-r--r--g_constrnew.ml410858logplain
-rw-r--r--g_ltac.ml48294logplain
-rw-r--r--g_ltacnew.ml47092logplain
-rw-r--r--g_minicoq.ml45440logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_module.ml41305logplain
-rw-r--r--g_natsyntax.ml6039logplain
-rw-r--r--g_natsyntax.mli572logplain
-rw-r--r--g_natsyntaxnew.mli572logplain
-rw-r--r--g_prim.ml45307logplain
-rw-r--r--g_primnew.ml44967logplain
-rw-r--r--g_proofs.ml45437logplain
-rw-r--r--g_proofsnew.ml44976logplain
-rw-r--r--g_rsyntax.ml11290logplain
-rw-r--r--g_tactic.ml414669logplain
-rw-r--r--g_tacticnew.ml416014logplain
-rw-r--r--g_vernac.ml417313logplain
-rw-r--r--g_vernacnew.ml425767logplain
-rw-r--r--g_zsyntax.ml12843logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--g_zsyntaxnew.mli572logplain
-rw-r--r--lexer.ml417633logplain
-rw-r--r--lexer.mli1464logplain
-rw-r--r--pcoq.ml426871logplain
-rw-r--r--pcoq.mli6320logplain
-rw-r--r--ppconstr.ml12299logplain
-rw-r--r--ppconstr.mli1476logplain
-rw-r--r--pptactic.ml28797logplain
-rw-r--r--pptactic.mli3120logplain
-rw-r--r--prettyp.ml20336logplain
-rw-r--r--prettyp.mli2401logplain
-rw-r--r--printer.ml8242logplain
-rw-r--r--printer.mli2111logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_coqast.ml424378logplain
-rw-r--r--q_util.ml42341logplain
-rw-r--r--q_util.mli1064logplain
-rw-r--r--search.ml6967logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml49419logplain
-rw-r--r--termast.ml16978logplain
-rw-r--r--termast.mli1901logplain
-rw-r--r--vernacextend.ml45191logplain