aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/prettyp.ml
Commit message (Expand)AuthorAge
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-02-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Correction ordre d'affichage des champs des RecordGravatar herbelin2007-12-14
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Correction de quelques défauts d'affichage (notations sous "as" pourGravatar herbelin2007-10-05
* Réaffichage des Structure/Record sous la forme RecordGravatar herbelin2007-05-28
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Suite ajout option -output-contextGravatar herbelin2006-12-08
* Ajout d'une option -output-context qui affiche le contexte en CCI pur à laGravatar herbelin2006-12-08
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Ajout option Set Printing Universes et amélioration affichage des universGravatar herbelin2006-10-28
* Déplacement surround dans util.ml et parenthésage des déclarationsGravatar herbelin2006-09-23
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Correction bug Inspect introduit par le passage du discharge à une méthode ...Gravatar herbelin2006-01-28
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* pas besoin de List.length pour savoir si une liste est videGravatar letouzey2005-08-19
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
* Nouvelle mouture Print Canonical StructuresGravatar herbelin2005-02-12
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Amélioration message LocateGravatar herbelin2005-01-13
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Amélioration message localisation constructions et modulesGravatar herbelin2004-12-09
* 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