aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--cLexer.ml424990logplain
-rw-r--r--cLexer.mli1945logplain
-rw-r--r--doc.tex221logplain
-rw-r--r--egramcoq.ml18478logplain
-rw-r--r--egramcoq.mli879logplain
-rw-r--r--egramml.ml2840logplain
-rw-r--r--egramml.mli1329logplain
-rw-r--r--g_constr.ml419548logplain
-rw-r--r--g_prim.ml43453logplain
-rw-r--r--g_proofs.ml44703logplain
-rw-r--r--g_vernac.ml445216logplain
-rw-r--r--parsing.mllib67logplain
-rw-r--r--pcoq.ml21186logplain
-rw-r--r--pcoq.mli11094logplain
-rw-r--r--tok.ml3544logplain
-rw-r--r--tok.mli1108logplain