aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml412056logplain
-rwxr-xr-xast.ml18771logplain
-rwxr-xr-xast.mli3500logplain
-rw-r--r--coqast.ml4060logplain
-rw-r--r--coqast.mli1626logplain
-rw-r--r--egrammar.ml18522logplain
-rw-r--r--egrammar.mli1795logplain
-rw-r--r--esyntax.ml9481logplain
-rw-r--r--esyntax.mli1844logplain
-rw-r--r--extend.ml11767logplain
-rw-r--r--extend.mli4337logplain
-rw-r--r--g_basevernac.ml419612logplain
-rw-r--r--g_cases.ml42633logplain
-rw-r--r--g_constr.ml413307logplain
-rw-r--r--g_constrnew.ml410819logplain
-rw-r--r--g_ltac.ml48287logplain
-rw-r--r--g_ltacnew.ml47085logplain
-rw-r--r--g_minicoq.ml45433logplain
-rw-r--r--g_minicoq.mli995logplain
-rw-r--r--g_module.ml41298logplain
-rw-r--r--g_natsyntax.ml6029logplain
-rw-r--r--g_natsyntax.mli565logplain
-rw-r--r--g_natsyntaxnew.mli565logplain
-rw-r--r--g_prim.ml45300logplain
-rw-r--r--g_primnew.ml44960logplain
-rw-r--r--g_proofs.ml45430logplain
-rw-r--r--g_proofsnew.ml44969logplain
-rw-r--r--g_rsyntax.ml11282logplain
-rw-r--r--g_tactic.ml414524logplain
-rw-r--r--g_tacticnew.ml415824logplain
-rw-r--r--g_vernac.ml417306logplain
-rw-r--r--g_vernacnew.ml425764logplain
-rw-r--r--g_zsyntax.ml12831logplain
-rw-r--r--g_zsyntax.mli565logplain
-rw-r--r--g_zsyntaxnew.mli565logplain
-rw-r--r--lexer.ml416963logplain
-rw-r--r--lexer.mli1405logplain
-rw-r--r--pcoq.ml426317logplain
-rw-r--r--pcoq.mli6313logplain
-rw-r--r--ppconstr.ml11703logplain
-rw-r--r--ppconstr.mli1469logplain
-rw-r--r--pptactic.ml28361logplain
-rw-r--r--pptactic.mli3113logplain
-rw-r--r--prettyp.ml19431logplain
-rw-r--r--prettyp.mli2394logplain
-rw-r--r--printer.ml8235logplain
-rw-r--r--printer.mli2104logplain
-rw-r--r--printmod.ml4873logplain
-rw-r--r--printmod.mli742logplain
-rw-r--r--q_coqast.ml424371logplain
-rw-r--r--q_util.ml42346logplain
-rw-r--r--q_util.mli1057logplain
-rw-r--r--search.ml6960logplain
-rw-r--r--search.mli2101logplain
-rw-r--r--tacextend.ml49360logplain
-rw-r--r--termast.ml16971logplain
-rw-r--r--termast.mli1894logplain
-rw-r--r--vernacextend.ml45166logplain