aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml49875logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13056logplain
-rw-r--r--egrammar.mli2118logplain
-rw-r--r--extend.ml1796logplain
-rw-r--r--extend.mli1722logplain
-rw-r--r--g_ascii_syntax.ml2705logplain
-rw-r--r--g_constr.ml416743logplain
-rw-r--r--g_decl_mode.ml47902logplain
-rw-r--r--g_intsyntax.ml10040logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml47883logplain
-rw-r--r--g_minicoq.ml45476logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_natsyntax.ml2377logplain
-rw-r--r--g_natsyntax.mli572logplain
-rw-r--r--g_prim.ml42633logplain
-rw-r--r--g_proofs.ml45121logplain
-rw-r--r--g_rsyntax.ml4199logplain
-rw-r--r--g_string_syntax.ml2124logplain
-rw-r--r--g_tactic.ml418876logplain
-rw-r--r--g_vernac.ml431186logplain
-rw-r--r--g_xml.ml410180logplain
-rw-r--r--g_zsyntax.ml6669logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--lexer.ml421183logplain
-rw-r--r--lexer.mli1506logplain
-rw-r--r--pcoq.ml423930logplain
-rw-r--r--pcoq.mli8229logplain
-rw-r--r--ppconstr.ml23320logplain
-rw-r--r--ppconstr.mli2670logplain
-rw-r--r--ppdecl_proof.ml6439logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml38897logplain
-rw-r--r--pptactic.mli3470logplain
-rw-r--r--ppvernac.ml35664logplain
-rw-r--r--ppvernac.mli795logplain
-rw-r--r--prettyp.ml26802logplain
-rw-r--r--prettyp.mli3623logplain
-rw-r--r--printer.ml16147logplain
-rw-r--r--printer.mli4558logplain
-rw-r--r--printmod.ml5824logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44359logplain
-rw-r--r--q_coqast.ml422371logplain
-rw-r--r--q_util.ml44964logplain
-rw-r--r--q_util.mli1152logplain
-rw-r--r--search.ml6976logplain
-rw-r--r--search.mli2108logplain
-rw-r--r--tacextend.ml47172logplain
-rw-r--r--tactic_printer.ml6995logplain
-rw-r--r--tactic_printer.mli1022logplain
-rw-r--r--vernacextend.ml43929logplain