aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml410661logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13487logplain
-rw-r--r--egrammar.mli2118logplain
-rw-r--r--extend.ml1795logplain
-rw-r--r--extend.mli1721logplain
-rw-r--r--g_ascii_syntax.ml2705logplain
-rw-r--r--g_constr.ml416214logplain
-rw-r--r--g_decl_mode.ml47902logplain
-rw-r--r--g_intsyntax.ml10208logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml48391logplain
-rw-r--r--g_minicoq.mli1002logplain
-rw-r--r--g_natsyntax.ml2377logplain
-rw-r--r--g_natsyntax.mli642logplain
-rw-r--r--g_prim.ml42991logplain
-rw-r--r--g_proofs.ml45476logplain
-rw-r--r--g_rsyntax.ml4198logplain
-rw-r--r--g_string_syntax.ml2123logplain
-rw-r--r--g_tactic.ml423852logplain
-rw-r--r--g_vernac.ml431709logplain
-rw-r--r--g_xml.ml410166logplain
-rw-r--r--g_zsyntax.ml6649logplain
-rw-r--r--g_zsyntax.mli572logplain
-rw-r--r--lexer.ml417406logplain
-rw-r--r--lexer.mli1506logplain
-rw-r--r--pcoq.ml425570logplain
-rw-r--r--pcoq.mli8635logplain
-rw-r--r--ppconstr.ml24058logplain
-rw-r--r--ppconstr.mli2741logplain
-rw-r--r--ppdecl_proof.ml6438logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml39949logplain
-rw-r--r--pptactic.mli3530logplain
-rw-r--r--ppvernac.ml36554logplain
-rw-r--r--ppvernac.mli795logplain
-rw-r--r--prettyp.ml27432logplain
-rw-r--r--prettyp.mli3667logplain
-rw-r--r--printer.ml17059logplain
-rw-r--r--printer.mli4952logplain
-rw-r--r--printmod.ml5831logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44368logplain
-rw-r--r--q_coqast.ml423115logplain
-rw-r--r--q_util.ml45189logplain
-rw-r--r--q_util.mli1305logplain
-rw-r--r--tacextend.ml47173logplain
-rw-r--r--tactic_printer.ml7126logplain
-rw-r--r--tactic_printer.mli1042logplain
-rw-r--r--vernacextend.ml44091logplain