aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
ModeNameSize
-rw-r--r--genprint.ml1940logplain
-rw-r--r--genprint.mli1265logplain
-rw-r--r--ppconstr.ml21664logplain
-rw-r--r--ppconstr.mli3717logplain
-rw-r--r--pptactic.ml37198logplain
-rw-r--r--pptactic.mli3986logplain
-rw-r--r--pputils.ml702logplain
-rw-r--r--pputils.mli665logplain
-rw-r--r--ppvernac.ml37332logplain
-rw-r--r--ppvernac.mli880logplain
-rw-r--r--prettyp.ml27460logplain
-rw-r--r--prettyp.mli3222logplain
-rw-r--r--printer.ml26865logplain
-rw-r--r--printer.mli6594logplain
-rw-r--r--printing.mllib60logplain
-rw-r--r--printmod.ml10519logplain
-rw-r--r--printmod.mli749logplain