aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml4
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added a function that escapes XML characters in ppcmds.Gravatar cek2008-04-16
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Correction de quelques défauts d'affichage (notations sous "as" pourGravatar herbelin2007-10-05
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Modification of emacs output: Pp.warning and al now output warningGravatar courtieu2006-04-27
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Nouvelle en-têteGravatar herbelin2004-07-16
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* warning vers std_errGravatar herbelin2003-09-10
* *** empty log message ***Gravatar barras2003-03-21
* interface GTK2 experimentaleGravatar monate2003-02-04
* reparation du make depend et du .dependGravatar letouzey2001-12-19