aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
ModeNameSize
-rw-r--r--genprint.ml1635logplain
-rw-r--r--genprint.mli1265logplain
-rw-r--r--miscprint.ml1892logplain
-rw-r--r--miscprint.mli978logplain
-rw-r--r--ppannotation.ml626logplain
-rw-r--r--ppannotation.mli753logplain
-rw-r--r--ppconstr.ml27055logplain
-rw-r--r--ppconstr.mli1173logplain
-rw-r--r--ppconstrsig.mli3803logplain
-rw-r--r--pptactic.ml42593logplain
-rw-r--r--pptactic.mli3999logplain
-rw-r--r--pputils.ml702logplain
-rw-r--r--pputils.mli665logplain
-rw-r--r--ppvernac.ml42288logplain
-rw-r--r--ppvernac.mli549logplain
-rw-r--r--ppvernacsig.mli773logplain
-rw-r--r--prettyp.ml29809logplain
-rw-r--r--prettyp.mli3396logplain
-rw-r--r--printer.ml30353logplain
-rw-r--r--printer.mli7377logplain
-rw-r--r--printing.mllib106logplain
-rw-r--r--printmod.ml10772logplain
-rw-r--r--printmod.mli749logplain