index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
prettyp.ml
Commit message (
Expand
)
Author
Age
...
*
Renaming Print Canonical Structure into Print Canonical Projections
herbelin
2005-02-18
*
Nouvelle mouture Print Canonical Structures
herbelin
2005-02-12
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
Amélioration message Locate
herbelin
2005-01-13
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Amélioration message localisation constructions et modules
herbelin
2004-12-09
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)
herbelin
2004-06-03
*
Affichage de l'opacité dans Print et About
herbelin
2004-06-02
*
Correction oubli du cas pas d'arguments implicites du tout
herbelin
2004-03-02
*
Expansion du type par nécessité dans le cas d'affichage d'implicites
herbelin
2004-02-28
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
Ajout Print Implicit avec depliage du type
herbelin
2003-11-15
*
Saut de ligne avant les infos non logiques de print_about
herbelin
2003-10-23
*
Extension de Locate
herbelin
2003-10-21
*
Ameliration affichage inductifs
herbelin
2003-10-13
*
Ajout fnl() dans About
herbelin
2003-10-11
*
Inspect saute maintenant les marqueurs invisibles
herbelin
2003-10-07
*
Bug about
herbelin
2003-09-26
*
Ajout 'About'
herbelin
2003-09-26
*
Mise en place d'implicites par noms en v8
herbelin
2003-09-21
*
Affichage des scopes d'arguments
herbelin
2003-09-12
*
Impression sans ',' des constructeurs de meme type, pour v8
herbelin
2003-09-05
*
Affichage des inductifs en v8
herbelin
2003-08-31
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...
herbelin
2003-02-27
*
Pour satisfaire ProofGeneral
coq
2003-01-31
*
Deux p\'tits trucs ;)
coq
2003-01-27
*
Petit netoyage dans lib
coq
2002-12-19
*
possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...
letouzey
2002-12-13
*
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
letouzey
2002-12-03
*
Réaffichage des Syntactic Definition (printer constr_expr).
herbelin
2002-11-26
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-28
*
Restriction sur la forme des Syntactic Definition et re-localisation en fonct...
herbelin
2002-10-12
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
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
*
Typo
herbelin
2002-04-16
*
Bug affichage '++' au lieu de ';'
herbelin
2001-12-21
*
affichage correct du type des inductifs et constructeurs en presence
barras
2001-12-18
[prev]
[next]