aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore133logplain
-rw-r--r--argextend.ml48666logplain
-rwxr-xr-xast.ml18775logplain
-rwxr-xr-xast.mli3492logplain
-rw-r--r--coqast.ml4060logplain
-rw-r--r--coqast.mli1626logplain
-rw-r--r--egrammar.ml18566logplain
-rw-r--r--egrammar.mli1808logplain
-rw-r--r--esyntax.ml9474logplain
-rw-r--r--esyntax.mli1860logplain
-rw-r--r--extend.ml11289logplain
-rw-r--r--extend.mli4092logplain
-rw-r--r--g_basevernac.ml416345logplain
-rw-r--r--g_cases.ml42303logplain
-rw-r--r--g_constr.ml412026logplain
-rw-r--r--g_constrnew.ml48003logplain
-rw-r--r--g_ltac.ml48672logplain
-rw-r--r--g_ltacnew.ml47017logplain
-rw-r--r--g_minicoq.ml45433logplain
-rw-r--r--g_minicoq.mli995logplain
-rw-r--r--g_module.ml41282logplain
-rw-r--r--g_natsyntax.ml5999logplain
-rw-r--r--g_natsyntax.mli565logplain
-rw-r--r--g_natsyntaxnew.ml5204logplain
-rw-r--r--g_natsyntaxnew.mli565logplain
-rw-r--r--g_prim.ml45250logplain
-rw-r--r--g_primnew.ml44701logplain
-rw-r--r--g_proofs.ml45162logplain
-rw-r--r--g_proofsnew.ml45293logplain
-rw-r--r--g_rsyntax.ml9934logplain
-rw-r--r--g_rsyntaxnew.ml3915logplain
-rw-r--r--g_tactic.ml412704logplain
-rw-r--r--g_tacticnew.ml412917logplain
-rw-r--r--g_vernac.ml417066logplain
-rw-r--r--g_vernacnew.ml428826logplain
-rw-r--r--g_zsyntax.ml10632logplain
-rw-r--r--g_zsyntax.mli565logplain
-rw-r--r--g_zsyntaxnew.ml5798logplain
-rw-r--r--g_zsyntaxnew.mli565logplain
-rw-r--r--lexer.ml414298logplain
-rw-r--r--lexer.mli1260logplain
-rw-r--r--pcoq.ml419305logplain
-rw-r--r--pcoq.mli5614logplain
-rw-r--r--ppconstr.ml10843logplain
-rw-r--r--ppconstr.mli1399logplain
-rw-r--r--pptactic.ml22551logplain
-rw-r--r--pptactic.mli1891logplain
-rw-r--r--prettyp.ml15289logplain
-rw-r--r--prettyp.mli2224logplain
-rw-r--r--printer.ml7978logplain
-rw-r--r--printer.mli2104logplain
-rw-r--r--printmod.ml4556logplain
-rw-r--r--printmod.mli742logplain
-rw-r--r--q_coqast.ml423339logplain
-rw-r--r--q_util.ml42256logplain
-rw-r--r--q_util.mli1016logplain
-rw-r--r--search.ml7418logplain
-rw-r--r--search.mli1842logplain
-rw-r--r--tacextend.ml48613logplain
-rw-r--r--termast.ml14374logplain
-rw-r--r--termast.mli1882logplain
-rw-r--r--vernacextend.ml46316logplain