summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml49927logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13301logplain
-rw-r--r--egrammar.mli2169logplain
-rw-r--r--extend.ml1843logplain
-rw-r--r--extend.mli1770logplain
-rw-r--r--g_ascii_syntax.ml2760logplain
-rw-r--r--g_constr.ml414806logplain
-rw-r--r--g_decl_mode.ml47956logplain
-rw-r--r--g_intsyntax.ml10259logplain
-rw-r--r--g_intsyntax.mli586logplain
-rw-r--r--g_ltac.ml47894logplain
-rw-r--r--g_minicoq.ml45528logplain
-rw-r--r--g_minicoq.mli1053logplain
-rw-r--r--g_natsyntax.ml2430logplain
-rw-r--r--g_natsyntax.mli696logplain
-rw-r--r--g_prim.ml42680logplain
-rw-r--r--g_proofs.ml45171logplain
-rw-r--r--g_rsyntax.ml4249logplain
-rw-r--r--g_string_syntax.ml2180logplain
-rw-r--r--g_tactic.ml423149logplain
-rw-r--r--g_vernac.ml431445logplain
-rw-r--r--g_xml.ml410227logplain
-rw-r--r--g_zsyntax.ml6698logplain
-rw-r--r--g_zsyntax.mli623logplain
-rw-r--r--lexer.ml416484logplain
-rw-r--r--lexer.mli1553logplain
-rw-r--r--pcoq.ml425558logplain
-rw-r--r--pcoq.mli8654logplain
-rw-r--r--ppconstr.ml23734logplain
-rw-r--r--ppconstr.mli2832logplain
-rw-r--r--ppdecl_proof.ml6492logplain
-rw-r--r--ppdecl_proof.mli78logplain
-rw-r--r--pptactic.ml39632logplain
-rw-r--r--pptactic.mli3520logplain
-rw-r--r--ppvernac.ml36444logplain
-rw-r--r--ppvernac.mli845logplain
-rw-r--r--prettyp.ml27304logplain
-rw-r--r--prettyp.mli3672logplain
-rw-r--r--printer.ml16503logplain
-rw-r--r--printer.mli4886logplain
-rw-r--r--printmod.ml5824logplain
-rw-r--r--printmod.mli749logplain
-rw-r--r--q_constr.ml44410logplain
-rw-r--r--q_coqast.ml422510logplain
-rw-r--r--q_util.ml45013logplain
-rw-r--r--q_util.mli1200logplain
-rw-r--r--search.ml7029logplain
-rw-r--r--search.mli2156logplain
-rw-r--r--tacextend.ml47224logplain
-rw-r--r--tactic_printer.ml7452logplain
-rw-r--r--tactic_printer.mli1078logplain
-rw-r--r--vernacextend.ml43984logplain