coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Oups: thanks to ./configure -reals no, I was not building the whole dependenc...	letouzey	2007-06-26
*	additional properties for FMap (and slight rework of SetoidList and FSetPrope...	letouzey	2007-06-26
*	Simplification de la construction du .depend:	notin	2007-06-21
*	Adding: Field instance for Q.	roconnor	2007-06-21
*	Extension of NArith: Nminus, Nmin, etc	letouzey	2007-06-07
*	A tentative fix for bug #1455	lmamane	2007-03-22
*	màj dépendances .v: SubtacTactics.vo	lmamane	2007-03-06
*	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau	2007-02-19
*	Fix mistake naming my Tactics file Tactics :)	msozeau	2007-02-07
*	complement du commit 9591	bgregoir	2007-02-05
*	Updated Makefile to include ConstructiveEpsilon.v	emakarov	2007-01-23
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir	2006-12-15
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Exports manquants dans ring	barras	2006-10-29
*	simplif de la partie ML de ring/field	barras	2006-10-27
*	changement des _sym par _comm dans setoid_ring	bgregoir	2006-10-27
*	Ajout ListTactics	herbelin	2006-10-27
*	oups, ne chargeait pas les bons fichiers	letouzey	2006-10-25
*	conflit de nom (Field_theory) modulo la casse	barras	2006-10-25
*	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras	2006-10-05
*	separation de RealField	barras	2006-09-28
*	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
*	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey	2006-06-25
*	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin	2006-06-09
*	Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...	letouzey	2006-06-05
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
*	ajout de QArith dans les theories standards	letouzey	2006-05-31
*	un debut de propriétés concernant FMap	letouzey	2006-05-22
*	Dépendances pour List.v	notin	2006-05-18
*	etoffage des notions de permutations (a la fois List.Permutation et Permutati...	letouzey	2006-05-16
*	ajout de theories/FSets/DecidableTypeEx.v	letouzey	2006-05-15
*	ajout d'exemples de decidable types	letouzey	2006-05-15
*	Duplication du fichier FSetProperties pour les ensembles Weak.	letouzey	2006-05-11
*	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest	2006-05-03
*	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey	2006-04-29
*	Régénération après mise à jour coqdep pour traiter Require multiple	herbelin	2006-04-26
*	Un gros coup de lifting pour IntMap:	letouzey	2006-04-25
*	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey	2006-04-06
*	reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...	letouzey	2006-03-28
*	ajout d'un debut de proprietes pour les FSetWeak	letouzey	2006-03-17
*	Ajout de theories/FSets contenant la partie "light" de FSets et FMap:	letouzey	2006-03-15
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	maj	coq	2006-02-22
*	Zmax et Zminmax	herbelin	2006-02-12