coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction du bug #1510	notin	2007-04-17
*	Correction bug #1499	notin	2007-04-13
*	Transparency of Z_lt_le_dec	notin	2007-04-12
*	simplier version of tail_plus	letouzey	2007-04-06
*	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov	2007-04-02
*	Réparation de NArith/BinPos.v suite au commit #9739	notin	2007-04-02
*	Removed the definition of extensions of apply to equivalences	emakarov	2007-04-01
*	Added the following theorems to BinPos:	emakarov	2007-03-30
*	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov	2007-03-30
*	stupid me: ?f two times in a pattern	letouzey	2007-03-26
*	PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...	letouzey	2007-03-26
*	Typos	herbelin	2007-03-15
*	Removed an unnecessary argument (p : positive) in Prect_base.	emakarov	2007-03-14
*	Proof simplification for eq_nat_dec et le_lt_dec: induction over	letouzey	2007-03-12
*	Transparence de eq_dec et lt_dec daans OrderedTypeFacts	notin	2007-03-08
*	FSetInterface: new item choose_equal in the spec S (request of P. Casteran)	letouzey	2007-02-28
*	Ajouts de lemmes dans Min et Max	notin	2007-02-19
*	Autres passages de Set Ã Type dans Relations et Wellfounded	herbelin	2007-02-12
*	Backtrack sur le passage de Set à Type pour l'ordre lexicographique	herbelin	2007-02-07
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
*	Correction typo eq_rec_eq (cf bug #1339)	herbelin	2007-01-31
*	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov	2007-01-23
*	Clarification redondance Axiome du choix unique/description	herbelin	2007-01-22
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	Remplacement de la définition de Pind et Prec par une définition	herbelin	2006-12-28
*	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir	2006-12-15
*	Dépendence inutile	herbelin	2006-12-12
*	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin	2006-12-12
*	Bug nommage Zgt_trans_succ	herbelin	2006-12-12
*	correction Open Local Scope (Ring)	bgregoir	2006-12-11
*	Changement dans le kernel :	bgregoir	2006-12-11
*	fixes PR#1269 about function: there is no reason well founded induction is	bertot	2006-11-05
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	LegacyRfield was opening R_scope	barras	2006-10-30
*	simplif de la partie ML de ring/field	barras	2006-10-27
*	Le caractère ² fait planter make doc	notin	2006-10-27
*	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin	2006-10-26
*	oups, ne chargeait pas les bons fichiers	letouzey	2006-10-25
*	Ajout de la tactique 'remember'	herbelin	2006-10-24
*	Noms "canoniques" pour certaines des propriétés de xor.	herbelin	2006-10-17
*	Mise en forme des theories	notin	2006-10-17
*	Ajout du théorème mult_minus_distr_l	notin	2006-10-13
*	revert, the previous commit was a mistake	bertot	2006-10-05
*	A version of natprering that should be more efficient and removal of a bad	bertot	2006-10-05
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
*	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras	2006-10-05
*	args implicites dans Field	barras	2006-09-29
*	separation de RealField	barras	2006-09-28
*	commit de field + renommages	barras	2006-09-26