summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--compat.ml48790logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egramcoq.ml14134logplain
-rw-r--r--egramcoq.mli2686logplain
-rw-r--r--egramml.ml2154logplain
-rw-r--r--egramml.mli1288logplain
-rw-r--r--g_constr.ml417345logplain
-rw-r--r--g_ltac.ml410206logplain
-rw-r--r--g_prim.ml43308logplain
-rw-r--r--g_proofs.ml46021logplain
-rw-r--r--g_tactic.ml426082logplain
-rw-r--r--g_vernac.ml443109logplain
-rw-r--r--g_xml.ml410561logplain
-rw-r--r--highparsing.mllib64logplain
-rw-r--r--lexer.ml421728logplain
-rw-r--r--lexer.mli1155logplain
-rw-r--r--parsing.mllib39logplain
-rw-r--r--pcoq.ml428740logplain
-rw-r--r--pcoq.mli10595logplain
-rw-r--r--tok.ml3744logplain
-rw-r--r--tok.mli1105logplain