summaryrefslogtreecommitdiff
path: root/parsing
ModeNameSize
-rw-r--r--cLexer.ml424383logplain
-rw-r--r--cLexer.mli1114logplain
-rw-r--r--compat.ml412690logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egramcoq.ml17866logplain
-rw-r--r--egramcoq.mli987logplain
-rw-r--r--egramml.ml2815logplain
-rw-r--r--egramml.mli1316logplain
-rw-r--r--g_constr.ml418145logplain
-rw-r--r--g_prim.ml43311logplain
-rw-r--r--g_proofs.ml46215logplain
-rw-r--r--g_tactic.ml425123logplain
-rw-r--r--g_vernac.ml445605logplain
-rw-r--r--highparsing.mllib43logplain
-rw-r--r--parsing.mllib40logplain
-rw-r--r--pcoq.ml18248logplain
-rw-r--r--pcoq.mli10025logplain
-rw-r--r--tok.ml3544logplain
-rw-r--r--tok.mli1108logplain