coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	Diverses corrections	herbelin	2008-04-14
*	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau	2008-04-12
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Encore des _sym au lieu de _comm	herbelin	2006-11-13
*	petits pbs de dependances	barras	2006-09-26
*	Compilation newring	notin	2006-09-26
*	commit de field + renommages	barras	2006-09-26
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	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