summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml49927logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13397logplain
-rw-r--r--egrammar.mli2169logplain
-rw-r--r--extend.ml1843logplain
-rw-r--r--extend.mli1770logplain
-rw-r--r--g_ascii_syntax.ml2761logplain
-rw-r--r--g_constr.ml415166logplain
-rw-r--r--g_decl_mode.ml47956logplain
-rw-r--r--g_intsyntax.ml10261logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml47889logplain
-rw-r--r--g_minicoq.mli1053logplain
-rw-r--r--g_natsyntax.ml2430logplain
-rw-r--r--g_natsyntax.mli696logplain
-rw-r--r--g_prim.ml43043logplain
-rw-r--r--g_proofs.ml45171logplain
-rw-r--r--g_rsyntax.ml4249logplain
-rw-r--r--g_string_syntax.ml2180logplain
-rw-r--r--g_tactic.ml423923logplain
-rw-r--r--g_vernac.ml431446logplain
-rw-r--r--g_xml.ml410214logplain
-rw-r--r--g_zsyntax.ml6700logplain
-rw-r--r--g_zsyntax.mli623logplain
-rw-r--r--lexer.ml416821logplain
-rw-r--r--lexer.mli1553logplain
-rw-r--r--pcoq.ml425537logplain
-rw-r--r--pcoq.mli8636logplain
-rw-r--r--ppconstr.ml23581logplain
-rw-r--r--ppconstr.mli2768logplain
-rw-r--r--ppdecl_proof.ml6492logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml39654logplain
-rw-r--r--pptactic.mli3581logplain
-rw-r--r--ppvernac.ml36103logplain
-rw-r--r--ppvernac.mli845logplain
-rw-r--r--prettyp.ml27340logplain
-rw-r--r--prettyp.mli3672logplain
-rw-r--r--printer.ml16934logplain
-rw-r--r--printer.mli5002logplain
-rw-r--r--printmod.ml5824logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44410logplain
-rw-r--r--q_coqast.ml422660logplain
-rw-r--r--q_util.ml45238logplain
-rw-r--r--q_util.mli1354logplain
-rw-r--r--search.ml7030logplain
-rw-r--r--search.mli2156logplain
-rw-r--r--tacextend.ml47225logplain
-rw-r--r--tactic_printer.ml7180logplain
-rw-r--r--tactic_printer.mli1097logplain
-rw-r--r--vernacextend.ml43984logplain