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