aboutsummaryrefslogtreecommitdiff
path: root/lib/pp.ml4
AgeCommit message (Collapse)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16Added a function that escapes XML characters in ppcmds.cek
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10803 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-05Correction de quelques défauts d'affichage (notations sous "as" pourherbelin
filtrage; sauts de line intempestifs dans pretty.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par ↵herbelin
compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Modification of emacs output: Pp.warning and al now output warningcourtieu
between special characters. I had to add a hidden variable print_emacs and a function to set it to true in Pp because using Options.print_emacs would have introduce a circularity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8747 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Remplacement Pp.qs par Pptactic.qsnewherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10warning vers std_errherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4346 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-04interface GTK2 experimentalemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19reparation du make depend et du .dependletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:24:35 +0000