aboutsummaryrefslogtreecommitdiff
path: root/parsing/prettyp.mli
AgeCommit message (Expand)Author
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2006-12-08Suite ajout option -output-contextherbelin
2006-12-08Ajout d'une option -output-context qui affiche le contexte en CCI pur à laherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2004-07-16Nouvelle en-têteherbelin
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
2003-09-26Ajout 'About'herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-05-28Pretty -> Prettypfilliatr