aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--argextend.ml411009logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egrammar.ml12258logplain
-rw-r--r--egrammar.mli2097logplain
-rw-r--r--extend.ml1412logplain
-rw-r--r--extend.mli1401logplain
-rw-r--r--extrawit.ml2068logplain
-rw-r--r--extrawit.mli2234logplain
-rw-r--r--g_constr.ml415543logplain
-rw-r--r--g_intsyntax.mli587logplain
-rw-r--r--g_ltac.ml48365logplain
-rw-r--r--g_natsyntax.mli629logplain
-rw-r--r--g_prim.ml43238logplain
-rw-r--r--g_proofs.ml45993logplain
-rw-r--r--g_tactic.ml425944logplain
-rw-r--r--g_vernac.ml435061logplain
-rw-r--r--g_xml.ml410135logplain
-rw-r--r--g_zsyntax.mli559logplain
-rw-r--r--grammar.mllib700logplain
-rw-r--r--highparsing.mllib50logplain
-rw-r--r--lexer.ml419077logplain
-rw-r--r--lexer.mli1215logplain
-rw-r--r--parsing.mllib94logplain
-rw-r--r--pcoq.ml425842logplain
-rw-r--r--pcoq.mli10197logplain
-rw-r--r--ppconstr.ml21638logplain
-rw-r--r--ppconstr.mli3563logplain
-rw-r--r--pptactic.ml40472logplain
-rw-r--r--pptactic.mli3668logplain
-rw-r--r--ppvernac.ml37964logplain
-rw-r--r--ppvernac.mli780logplain
-rw-r--r--prettyp.ml27358logplain
-rw-r--r--prettyp.mli3704logplain
-rw-r--r--printer.ml18272logplain
-rw-r--r--printer.mli5331logplain
-rw-r--r--printmod.ml5645logplain
-rw-r--r--printmod.mli750logplain
-rw-r--r--q_constr.ml44376logplain
-rw-r--r--q_coqast.ml424189logplain
-rw-r--r--q_util.ml42611logplain
-rw-r--r--q_util.mli1236logplain
-rw-r--r--tacextend.ml47293logplain
-rw-r--r--tactic_printer.ml5375logplain
-rw-r--r--tactic_printer.mli957logplain
-rw-r--r--tok.ml2955logplain
-rw-r--r--tok.mli1047logplain
-rw-r--r--vernacextend.ml43410logplain