aboutsummaryrefslogtreecommitdiff
path: root/printing/miscprint.ml
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
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
2016-06-16Fixing printing of pat%constr.Hugo Herbelin
2016-04-27Revert "Fixing printing of pat%constr."Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Hugo Herbelin
2016-04-27Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Hugo Herbelin
2016-04-27Revert "Fixing extra space in front of terminal in printing vernac."Hugo Herbelin
2016-04-27Fixing extra space in front of terminal in printing vernac.Hugo Herbelin
2016-04-27Revert "Protect printing of intro-patterns from collision when "[|" orHugo Herbelin
2016-04-27Protect printing of intro-patterns from collision when "[|" or "|]"Hugo Herbelin
2016-04-27Fixing printing of pat%constr.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
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