aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
ModeNameSize
-rw-r--r--cLexer.ml424725logplain
-rw-r--r--cLexer.mli2021logplain
-rw-r--r--egramcoq.ml18406logplain
-rw-r--r--egramcoq.mli1029logplain
-rw-r--r--egramml.ml2990logplain
-rw-r--r--egramml.mli1479logplain
-rw-r--r--extend.ml5010logplain
-rw-r--r--g_constr.ml419489logplain
-rw-r--r--g_prim.ml43657logplain
-rw-r--r--g_proofs.ml45705logplain
-rw-r--r--g_vernac.ml444431logplain
-rw-r--r--parsing.mllib85logplain
-rw-r--r--pcoq.ml21597logplain
-rw-r--r--pcoq.mli11508logplain
-rw-r--r--tok.ml3694logplain
-rw-r--r--tok.mli1258logplain
-rw-r--r--vernacexpr.ml19927logplain