summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml412388logplain
-rwxr-xr-xast.ml18831logplain
-rwxr-xr-xast.mli3561logplain
-rw-r--r--coqast.ml4122logplain
-rw-r--r--coqast.mli1692logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml19154logplain
-rw-r--r--egrammar.mli2052logplain
-rw-r--r--esyntax.ml9545logplain
-rw-r--r--esyntax.mli1907logplain
-rw-r--r--extend.ml11873logplain
-rw-r--r--extend.mli4492logplain
-rw-r--r--g_basevernac.ml419670logplain
-rw-r--r--g_cases.ml42698logplain
-rw-r--r--g_constr.ml413495logplain
-rw-r--r--g_constrnew.ml410926logplain
-rw-r--r--g_ltac.ml47790logplain
-rw-r--r--g_ltacnew.ml46591logplain
-rw-r--r--g_minicoq.ml45500logplain
-rw-r--r--g_minicoq.mli1062logplain
-rw-r--r--g_module.ml41363logplain
-rw-r--r--g_natsyntax.ml6100logplain
-rw-r--r--g_natsyntax.mli634logplain
-rw-r--r--g_natsyntaxnew.mli636logplain
-rw-r--r--g_prim.ml44267logplain
-rw-r--r--g_primnew.ml42513logplain
-rw-r--r--g_proofs.ml45496logplain
-rw-r--r--g_proofsnew.ml45037logplain
-rw-r--r--g_rsyntax.ml11290logplain
-rw-r--r--g_tactic.ml414100logplain
-rw-r--r--g_tacticnew.ml415011logplain
-rw-r--r--g_vernac.ml417420logplain
-rw-r--r--g_vernacnew.ml425802logplain
-rw-r--r--g_zsyntax.ml13010logplain
-rw-r--r--g_zsyntax.mli631logplain
-rw-r--r--g_zsyntaxnew.mli634logplain
-rw-r--r--lexer.ml417917logplain
-rw-r--r--lexer.mli1520logplain
-rw-r--r--pcoq.ml427056logplain
-rw-r--r--pcoq.mli6432logplain
-rw-r--r--ppconstr.ml12317logplain
-rw-r--r--ppconstr.mli1536logplain
-rw-r--r--pptactic.ml28908logplain
-rw-r--r--pptactic.mli3180logplain
-rw-r--r--prettyp.ml19495logplain
-rw-r--r--prettyp.mli2459logplain
-rw-r--r--printer.ml8299logplain
-rw-r--r--printer.mli2171logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_coqast.ml424520logplain
-rw-r--r--q_util.ml42397logplain
-rw-r--r--q_util.mli1120logplain
-rw-r--r--search.ml7023logplain
-rw-r--r--search.mli2165logplain
-rw-r--r--tacextend.ml49479logplain
-rw-r--r--termast.ml17035logplain
-rw-r--r--termast.mli1959logplain
-rw-r--r--vernacextend.ml45253logplain