aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml411552logplain
-rwxr-xr-xast.ml18763logplain
-rwxr-xr-xast.mli3492logplain
-rw-r--r--coqast.ml4060logplain
-rw-r--r--coqast.mli1626logplain
-rw-r--r--egrammar.ml19001logplain
-rw-r--r--egrammar.mli1894logplain
-rw-r--r--esyntax.ml9497logplain
-rw-r--r--esyntax.mli1860logplain
-rw-r--r--extend.ml11767logplain
-rw-r--r--extend.mli4337logplain
-rw-r--r--g_basevernac.ml419181logplain
-rw-r--r--g_cases.ml42677logplain
-rw-r--r--g_constr.ml413326logplain
-rw-r--r--g_constrnew.ml410737logplain
-rw-r--r--g_ltac.ml48885logplain
-rw-r--r--g_ltacnew.ml46919logplain
-rw-r--r--g_minicoq.ml45433logplain
-rw-r--r--g_minicoq.mli995logplain
-rw-r--r--g_module.ml41302logplain
-rw-r--r--g_natsyntax.ml6019logplain
-rw-r--r--g_natsyntax.mli565logplain
-rw-r--r--g_natsyntaxnew.mli565logplain
-rw-r--r--g_prim.ml45256logplain
-rw-r--r--g_primnew.ml44809logplain
-rw-r--r--g_proofs.ml45398logplain
-rw-r--r--g_proofsnew.ml45504logplain
-rw-r--r--g_rsyntax.ml11992logplain
-rw-r--r--g_tactic.ml414036logplain
-rw-r--r--g_tacticnew.ml415776logplain
-rw-r--r--g_vernac.ml417612logplain
-rw-r--r--g_vernacnew.ml426985logplain
-rw-r--r--g_zsyntax.ml10714logplain
-rw-r--r--g_zsyntax.mli565logplain
-rw-r--r--g_zsyntaxnew.mli565logplain
-rw-r--r--lexer.ml416564logplain
-rw-r--r--lexer.mli1305logplain
-rw-r--r--pcoq.ml422452logplain
-rw-r--r--pcoq.mli5836logplain
-rw-r--r--ppconstr.ml11080logplain
-rw-r--r--ppconstr.mli1469logplain
-rw-r--r--pptactic.ml26556logplain
-rw-r--r--pptactic.mli3113logplain
-rw-r--r--prettyp.ml17742logplain
-rw-r--r--prettyp.mli2350logplain
-rw-r--r--printer.ml8156logplain
-rw-r--r--printer.mli2104logplain
-rw-r--r--printmod.ml4873logplain
-rw-r--r--printmod.mli742logplain
-rw-r--r--q_coqast.ml423462logplain
-rw-r--r--q_util.ml42256logplain
-rw-r--r--q_util.mli1016logplain
-rw-r--r--search.ml7205logplain
-rw-r--r--search.mli2046logplain
-rw-r--r--tacextend.ml48584logplain
-rw-r--r--termast.ml14896logplain
-rw-r--r--termast.mli1894logplain
-rw-r--r--vernacextend.ml45079logplain