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
*
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
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Marre des unrecognized objects
herbelin
2001-09-24
*
Amélioration affichage de print_leaf_entry
herbelin
2001-09-20
*
Transparent
barras
2001-09-20
[next]