summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml49893logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13101logplain
-rw-r--r--egrammar.mli2158logplain
-rw-r--r--extend.ml1843logplain
-rw-r--r--extend.mli1770logplain
-rw-r--r--g_ascii_syntax.ml2690logplain
-rw-r--r--g_constr.ml411465logplain
-rw-r--r--g_decl_mode.ml47913logplain
-rw-r--r--g_ltac.ml47583logplain
-rw-r--r--g_minicoq.ml45491logplain
-rw-r--r--g_minicoq.mli1053logplain
-rw-r--r--g_natsyntax.ml2335logplain
-rw-r--r--g_natsyntax.mli625logplain
-rw-r--r--g_prim.ml42478logplain
-rw-r--r--g_proofs.ml44998logplain
-rw-r--r--g_rsyntax.ml4184logplain
-rw-r--r--g_string_syntax.ml2109logplain
-rw-r--r--g_tactic.ml416383logplain
-rw-r--r--g_vernac.ml428205logplain
-rw-r--r--g_xml.ml410156logplain
-rw-r--r--g_zsyntax.ml6697logplain
-rw-r--r--g_zsyntax.mli623logplain
-rw-r--r--lexer.ml420503logplain
-rw-r--r--lexer.mli1553logplain
-rw-r--r--pcoq.ml422514logplain
-rw-r--r--pcoq.mli8115logplain
-rw-r--r--ppconstr.ml22066logplain
-rw-r--r--ppconstr.mli2426logplain
-rw-r--r--ppdecl_proof.ml6475logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml37509logplain
-rw-r--r--pptactic.mli3352logplain
-rw-r--r--ppvernac.ml32355logplain
-rw-r--r--ppvernac.mli845logplain
-rw-r--r--prettyp.ml19790logplain
-rw-r--r--prettyp.mli2458logplain
-rw-r--r--printer.ml13364logplain
-rw-r--r--printer.mli3882logplain
-rw-r--r--printmod.ml4880logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44308logplain
-rw-r--r--q_coqast.ml421358logplain
-rw-r--r--q_util.ml44982logplain
-rw-r--r--q_util.mli1200logplain
-rw-r--r--search.ml6945logplain
-rw-r--r--search.mli2156logplain
-rw-r--r--tacextend.ml47209logplain
-rw-r--r--tactic_printer.ml7399logplain
-rw-r--r--tactic_printer.mli1018logplain
-rw-r--r--vernacextend.ml43969logplain