coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	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-03
*	The statement of the compatibility theorem for addition and multiplication	sacerdot	2005-02-02
*	setoid_rewrite t; [tac]	sacerdot	2005-02-02
*	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-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot	2004-10-01
*	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot	2004-09-30
*	New syntax	sacerdot	2004-09-29
*	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-09-03
*	Setoid_replace.setoid_replace: last argument (that was supposed to be	sacerdot	2004-07-23
*	correction d'un bug de la tactique pour les semi setoid rings.	clrenard	2004-07-22
*	Nouvelle en-tête	herbelin	2004-07-16
*	eq and eqT are the same	barras	2004-06-25
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Ordre standard pour l'associativite	herbelin	2003-11-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Noms/énoncés plus canoniques	herbelin	2003-11-12
*	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin	2003-11-05
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	Ajout notations pour les expressions dans un anneau	herbelin	2003-10-28
*	Simplification preuve	herbelin	2003-10-28
*	Ajout NArithRing	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	distinguer interp_cs et interp_setcs	letouzey	2003-10-06
*	Cacher les .v8	herbelin	2003-10-03
*	oups	letouzey	2003-09-28
*	2 pbs de plus réglés concernant Setoid Ring:	letouzey	2003-09-28
*	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin	2003-09-26
*	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-22
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-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-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Notations arithmetiques	herbelin	2003-05-13
*	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07