coq - The formal proof system

Age	Commit message (Expand)	Author
2007-12-14	Correction ordre d'affichage des champs des Record	herbelin
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-10-05	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin
2007-05-28	Réaffichage des Structure/Record sous la forme Record	herbelin
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
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
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	Ajout option Set Printing Universes et amélioration affichage des univers	herbelin
2006-09-23	Déplacement surround dans util.ml et parenthésage des déclarations	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-01-28	Correction bug Inspect introduit par le passage du discharge à une méthode ...	herbelin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-11-21	Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-08-19	pas besoin de List.length pour savoir si une liste est vide	letouzey
2005-02-20	Keep ClosedSection marker for reset	herbelin
2005-02-18	Renaming Print Canonical Structure into Print Canonical Projections	herbelin
2005-02-12	Nouvelle mouture Print Canonical Structures	herbelin
2005-02-12	Ajout Print Canonical Structures	herbelin
2005-01-14	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot
2005-01-13	Amélioration message Locate	herbelin
2005-01-02	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2004-12-09	Amélioration message localisation constructions et modules	herbelin
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-06-03	Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)	herbelin
2004-06-02	Affichage de l'opacité dans Print et About	herbelin
2004-03-02	Correction oubli du cas pas d'arguments implicites du tout	herbelin
2004-02-28	Expansion du type par nécessité dans le cas d'affichage d'implicites	herbelin
2004-01-29	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin
2003-11-15	Ajout Print Implicit avec depliage du type	herbelin
2003-10-23	Saut de ligne avant les infos non logiques de print_about	herbelin
2003-10-21	Extension de Locate	herbelin
2003-10-13	Ameliration affichage inductifs	herbelin
2003-10-11	Ajout fnl() dans About	herbelin
2003-10-07	Inspect saute maintenant les marqueurs invisibles	herbelin
2003-09-26	Bug about	herbelin
2003-09-26	Ajout 'About'	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-12	Affichage des scopes d'arguments	herbelin
2003-09-05	Impression sans ',' des constructeurs de meme type, pour v8	herbelin
2003-08-31	Affichage des inductifs en v8	herbelin