coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	switch theories/Numbers from Set to Type (both the abstract and the bignum pa...	letouzey	2008-05-22
*	- Changement du code de Zplus pour accomoder ring qui sinon prend une	herbelin	2008-05-11
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	- Fix bug in unification not taking into account the right meta	msozeau	2008-04-27
*	Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression	notin	2008-03-28
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	one more substitution s/Set/Type/	letouzey	2008-03-04
*	Proposal of a nice notation for constructors xI and xO of type positive	letouzey	2008-02-10
*	one forgotten compatibility lemma	letouzey	2008-02-08
*	Keep the Z_scope local to this file.	roconnor	2008-01-24
*	Adding Zdiv_le_compat_l	thery	2008-01-22
*	A result about Zsgn(a/b), both for Zdiv and ZOdiv	letouzey	2007-11-10
*	First reasonably complete version of ZOdiv, including some properties	letouzey	2007-11-10
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...	jforest	2007-11-09
*	more about ZOdiv and ZOmod (still not finished)	letouzey	2007-11-09
*	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey	2007-11-08
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey	2007-11-06
*	Adding Qround.v (and helper lemmas and hints)	roconnor	2007-11-01
*	In agreement with Laurent Thery, start migration of auxiliary results	letouzey	2007-11-01
*	Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le	roconnor	2007-10-19
*	Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v	emakarov	2007-08-08
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
*	normalisation (by closure) was not performed under fixpoints	barras	2007-07-12
*	Transparency of Z_lt_le_dec	notin	2007-04-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
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	simplif de la partie ML de ring/field	barras	2006-10-27
*	Mise en forme des theories	notin	2006-10-17
*	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
*	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras	2006-10-05
*	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
*	Ajout de Zgcd_spec (compat.)	notin	2006-06-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
*	ajout de QArith dans les theories standards	letouzey	2006-05-31
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin	2006-05-23
*	On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos	letouzey	2006-05-14
*	typo	letouzey	2006-05-13
*	un Zgcd calculant dans coq	letouzey	2006-05-13
*	une fonction pouvant calculer le gcd en coq	letouzey	2006-05-11
*	un Zgcd general gardant trace des coefs	letouzey	2006-05-05
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Bug Scope	herbelin	2006-02-12