aboutsummaryrefslogtreecommitdiff
path: root/lib/pp_control.ml
AgeCommit message (Expand)Author
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-03-14[safe-string] lib/miscelaneaEmilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-05-21Changing the heuristic fixing bug #4241.Pierre Courtieu
2015-05-20Answering report #4241 (formatting of boxes not behaving regularlyHugo Herbelin
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2012-06-26Fixed string width printing in string_of_ppcmdsppedrot
2010-12-03Remove dead codeglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-01-27- Fixed various Overfull in documentation.herbelin
2008-05-10Correction bug #1842 + correction bug initialisation introduit dansherbelin
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
2004-07-16Nouvelle en-têteherbelin
2003-10-16Marge presqu'a 80, maximum indentation a 50 pour une meilleure lisibiliteherbelin
2003-03-26Ajout de Set Print Widthgregoire
2003-03-12*** empty log message ***barras
2003-02-04interface GTK2 experimentalemonate
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-03-15entetesfilliatr
1999-10-01deep_gp pour l'écriture dans un fichierfilliatr
1999-08-16Initial revisionfilliatr