summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml414000logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml13401logplain
-rw-r--r--egrammar.mli2522logplain
-rw-r--r--extend.ml1530logplain
-rw-r--r--extend.mli1460logplain
-rw-r--r--extrawit.ml2098logplain
-rw-r--r--extrawit.mli2234logplain
-rw-r--r--g_constr.ml415682logplain
-rw-r--r--g_ltac.ml48420logplain
-rw-r--r--g_prim.ml43238logplain
-rw-r--r--g_proofs.ml45200logplain
-rw-r--r--g_tactic.ml425228logplain
-rw-r--r--g_vernac.ml439576logplain
-rw-r--r--g_xml.ml410187logplain
-rw-r--r--grammar.mllib721logplain
-rw-r--r--highparsing.mllib50logplain
-rw-r--r--lexer.ml420434logplain
-rw-r--r--lexer.mli1245logplain
-rw-r--r--parsing.mllib94logplain
-rw-r--r--pcoq.ml426473logplain
-rw-r--r--pcoq.mli10152logplain
-rw-r--r--ppconstr.ml20931logplain
-rw-r--r--ppconstr.mli3730logplain
-rw-r--r--pptactic.ml39496logplain
-rw-r--r--pptactic.mli3680logplain
-rw-r--r--ppvernac.ml37769logplain
-rw-r--r--ppvernac.mli748logplain
-rw-r--r--prettyp.ml27412logplain
-rw-r--r--prettyp.mli3209logplain
-rw-r--r--printer.ml26478logplain
-rw-r--r--printer.mli6411logplain
-rw-r--r--printmod.ml10165logplain
-rw-r--r--printmod.mli750logplain
-rw-r--r--q_constr.ml44420logplain
-rw-r--r--q_coqast.ml424774logplain
-rw-r--r--q_util.ml42721logplain
-rw-r--r--q_util.mli1236logplain
-rw-r--r--tacextend.ml48144logplain
-rw-r--r--tactic_printer.ml5377logplain
-rw-r--r--tactic_printer.mli957logplain
-rw-r--r--tok.ml2955logplain
-rw-r--r--tok.mli1047logplain
-rw-r--r--vernacextend.ml43542logplain