coq - The formal proof system

Age	Commit message (Expand)	Author
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-02-06	Nettoyage et documentation de Library	herbelin
2005-02-03	Implemented a test for "Add [Semi] Setoid Ring" to check that the given	sacerdot
2005-02-03	Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "\|\|"	sacerdot
2005-02-02	The statement of the compatibility theorem for addition and multiplication	sacerdot
2005-02-02	setoid_rewrite t; [tac]	sacerdot
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-11-12	Changement dans les boxed values .	gregoire
2004-10-01	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot
2004-09-30	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot
2004-09-29	New syntax	sacerdot
2004-09-03	premiere reorganisation de l\'unification	barras
2004-09-03	Ported to the new implementation of setoid_*.	sacerdot
2004-09-03	The old implementation of (setoid_replace c1 with c2) used to replace	sacerdot
2004-07-23	Setoid_replace.setoid_replace: last argument (that was supposed to be	sacerdot
2004-07-22	correction d'un bug de la tactique pour les semi setoid rings.	clrenard
2004-07-16	Nouvelle en-tête	herbelin
2004-06-25	eq and eqT are the same	barras
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-14	Ordre standard pour l'associativite	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-12	Noms/énoncés plus canoniques	herbelin
2003-11-05	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin
2003-11-01	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-28	Ajout notations pour les expressions dans un anneau	herbelin
2003-10-28	Simplification preuve	herbelin
2003-10-22	Ajout NArithRing	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-10-06	distinguer interp_cs et interp_setcs	letouzey
2003-10-03	Cacher les .v8	herbelin
2003-09-28	oups	letouzey
2003-09-28	2 pbs de plus réglés concernant Setoid Ring:	letouzey
2003-09-26	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin
2003-09-22	commit accidentel d'une bidouille	letouzey
2003-09-22	suite (et fin) reparation Setoid Ring	letouzey
2003-09-22	tentative de rafraichissement de Setoid Ring	letouzey
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-05-13	Notations arithmetiques	herbelin
2003-04-09	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin