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