aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/prettyp.ml
Commit message (Expand)AuthorAge
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)Gravatar herbelin2004-06-03
* Affichage de l'opacité dans Print et AboutGravatar herbelin2004-06-02
* Correction oubli du cas pas d'arguments implicites du toutGravatar herbelin2004-03-02
* Expansion du type par nécessité dans le cas d'affichage d'implicitesGravatar herbelin2004-02-28
* Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...Gravatar herbelin2004-01-29
* Ajout Print Implicit avec depliage du typeGravatar herbelin2003-11-15
* Saut de ligne avant les infos non logiques de print_aboutGravatar herbelin2003-10-23
* Extension de LocateGravatar herbelin2003-10-21
* Ameliration affichage inductifsGravatar herbelin2003-10-13
* Ajout fnl() dans AboutGravatar herbelin2003-10-11
* Inspect saute maintenant les marqueurs invisiblesGravatar herbelin2003-10-07
* Bug aboutGravatar herbelin2003-09-26
* Ajout 'About'Gravatar herbelin2003-09-26
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
* Affichage des scopes d'argumentsGravatar herbelin2003-09-12
* Impression sans ',' des constructeurs de meme type, pour v8Gravatar herbelin2003-09-05
* Affichage des inductifs en v8Gravatar herbelin2003-08-31
* Tables logarithmiques pour les coercions + nettoyageGravatar herbelin2003-06-08
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...Gravatar herbelin2003-02-27
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* Deux p\'tits trucs ;)Gravatar coq2003-01-27
* Petit netoyage dans libGravatar coq2002-12-19
* possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...Gravatar letouzey2002-12-13
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Des critères plus fins d'analyse des implicites automatiques; meilleur affic...Gravatar herbelin2002-10-28
* Restriction sur la forme des Syntactic Definition et re-localisation en fonct...Gravatar herbelin2002-10-12
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* TypoGravatar herbelin2002-04-16
* Bug affichage '++' au lieu de ';'Gravatar herbelin2001-12-21
* affichage correct du type des inductifs et constructeurs en presenceGravatar barras2001-12-18
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Marre des unrecognized objectsGravatar herbelin2001-09-24
* Amélioration affichage de print_leaf_entryGravatar herbelin2001-09-20