aboutsummaryrefslogtreecommitdiff
path: root/printing/miscprint.mli
AgeCommit message (Expand)Author
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-01[printing] Remove duplicated printing function.Emilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey