coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-04-28	Déplacement des opérations sur bool dans l'état initial	herbelin
2007-04-25	Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création	herbelin
2007-04-17	Correction du bug #1510	notin
2007-04-13	Correction bug #1499	notin
2007-04-12	Transparency of Z_lt_le_dec	notin
2007-04-06	simplier version of tail_plus	letouzey
2007-04-02	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-01	Removed the definition of extensions of apply to equivalences	emakarov
2007-03-30	Added the following theorems to BinPos:	emakarov
2007-03-30	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov
2007-03-26	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-15	Typos	herbelin
2007-03-14	Removed an unnecessary argument (p : positive) in Prect_base.	emakarov
2007-03-12	Proof simplification for eq_nat_dec et le_lt_dec: induction over	letouzey
2007-03-08	Transparence de eq_dec et lt_dec daans OrderedTypeFacts	notin
2007-02-28	FSetInterface: new item choose_equal in the spec S (request of P. Casteran)	letouzey
2007-02-19	Ajouts de lemmes dans Min et Max	notin
2007-02-12	Autres passages de Set Ã Type dans Relations et Wellfounded	herbelin
2007-02-07	Backtrack sur le passage de Set à Type pour l'ordre lexicographique	herbelin
2007-02-06	Passage de Set à Type dans Relations et Wellfounded	herbelin
2007-01-31	Correction typo eq_rec_eq (cf bug #1339)	herbelin
2007-01-23	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov
2007-01-22	Clarification redondance Axiome du choix unique/description	herbelin
2007-01-02	Add f_equal case for 6 arguments.	msozeau
2006-12-28	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-15	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir
2006-12-12	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-11	correction Open Local Scope (Ring)	bgregoir
2006-12-11	Changement dans le kernel :	bgregoir
2006-11-05	fixes PR#1269 about function: there is no reason well founded induction is	bertot
2006-10-30	fixed field_simplify + changed precedence of let and fun in ltac	barras
2006-10-30	LegacyRfield was opening R_scope	barras
2006-10-27	simplif de la partie ML de ring/field	barras
2006-10-27	Le caractère ² fait planter make doc	notin
2006-10-26	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin
2006-10-25	oups, ne chargeait pas les bons fichiers	letouzey
2006-10-24	Ajout de la tactique 'remember'	herbelin
2006-10-17	Noms "canoniques" pour certaines des propriétés de xor.	herbelin
2006-10-17	Mise en forme des theories	notin
2006-10-13	Ajout du théorème mult_minus_distr_l	notin
2006-10-05	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