aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--.cvsignore143logplain
-rw-r--r--argextend.ml47800logplain
-rwxr-xr-xast.ml24274logplain
-rwxr-xr-xast.mli4446logplain
-rw-r--r--astterm.ml30550logplain
-rw-r--r--astterm.mli3823logplain
-rw-r--r--coqast.ml8118logplain
-rw-r--r--coqast.mli1582logplain
-rw-r--r--coqlib.ml10050logplain
-rw-r--r--coqlib.mli3647logplain
-rw-r--r--egrammar.ml9535logplain
-rw-r--r--egrammar.mli1292logplain
-rw-r--r--esyntax.ml8856logplain
-rw-r--r--esyntax.mli1635logplain
-rw-r--r--extend.ml7013logplain
-rw-r--r--extend.mli2565logplain
-rw-r--r--g_basevernac.ml412486logplain
-rw-r--r--g_cases.ml42175logplain
-rw-r--r--g_constr.ml49955logplain
-rw-r--r--g_ltac.ml49016logplain
-rw-r--r--g_minicoq.ml45476logplain
-rw-r--r--g_minicoq.mli995logplain
-rw-r--r--g_natsyntax.ml2797logplain
-rw-r--r--g_natsyntax.mli565logplain
-rw-r--r--g_prim.ml45029logplain
-rw-r--r--g_proofs.ml45057logplain
-rw-r--r--g_rsyntax.ml2414logplain
-rw-r--r--g_tactic.ml412956logplain
-rw-r--r--g_vernac.ml414727logplain
-rw-r--r--g_zsyntax.ml5110logplain
-rw-r--r--g_zsyntax.mli625logplain
-rw-r--r--genarg.ml4926logplain
-rw-r--r--genarg.mli8055logplain
-rw-r--r--lexer.ml49363logplain
-rw-r--r--lexer.mli1093logplain
-rw-r--r--pcoq.ml416623logplain
-rw-r--r--pcoq.mli5967logplain
-rw-r--r--ppconstr.ml5028logplain
-rw-r--r--ppconstr.mli1332logplain
-rw-r--r--pptactic.ml22010logplain
-rw-r--r--pptactic.mli1486logplain
-rw-r--r--pretty.ml18986logplain
-rw-r--r--prettyp.ml18671logplain
-rw-r--r--prettyp.mli2241logplain
-rw-r--r--printer.ml6791logplain
-rw-r--r--printer.mli2363logplain
-rw-r--r--q_coqast.ml421511logplain
-rw-r--r--q_util.ml42256logplain
-rw-r--r--q_util.mli1016logplain
-rw-r--r--search.ml5965logplain
-rw-r--r--search.mli1614logplain
-rw-r--r--tacextend.ml47342logplain
-rw-r--r--termast.ml13812logplain
-rw-r--r--termast.mli1876logplain
-rw-r--r--vernacextend.ml46115logplain