coq - The formal proof system

Age	Commit message (Expand)	Author
2008-03-16	Removed unneeded tactics from RelationClasses. Use	msozeau
2008-03-16	Minor fixes on setoid rewriting. Now uses definitions of [relation] and	msozeau
2008-03-07	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau
2008-03-06	Plug the new setoid implemtation in, leaving the original one commented	msozeau
2008-02-18	Petite correction suite à la révision 10571	notin
2008-02-09	Solde de code mort et petites optimisations sur lesquels je suis	herbelin
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-08	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin
2007-11-08	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey
2007-11-07	Replaced BinNat with a new version that is based on theories/Numbers/Natural/...	emakarov
2007-09-20	Changed the definition of Nminus in BinNat.v by removing comparison.	emakarov
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-07-24	fixed bug 1448 and 1674	barras
2007-07-24	fixed bug 1675: computing carrier from the relation type was not right	barras
2007-07-12	normalisation (by closure) was not performed under fixpoints	barras
2007-07-12	port de r9968: bug avec les ring calculatoires	barras
2007-06-07	Extension of NArith: Nminus, Nmin, etc	letouzey
2007-04-29	Orthographe en passant	herbelin
2007-02-07	doc de ring/field + option infinite -> completeness	barras
2007-02-05	changement dans ring specification du sign, division	bgregoir
2007-02-02	field: introduction de Get_goal	bgregoir
2007-02-02	ring: introduction de Get_goal	bgregoir
2007-02-02	Now 1/x * x simplifies to 1	thery
2007-01-24	changement de la fonction norm_subst	bgregoir
2007-01-23	ring : Correction du bug PR#1306	bgregoir
2006-12-15	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir
2006-12-11	Changement dans le kernel :	bgregoir
2006-11-16	pb avec r9379 + modifs dans ring	barras
2006-11-16	suite de r9362: reconnaissance de qqs injections entre nat, N et Z	barras
2006-11-10	generalisation de ring pour faire Ring_nf	barras
2006-10-30	fixed field_simplify + changed precedence of let and fun in ltac	barras
2006-10-29	Exports manquants dans ring	barras
2006-10-27	simplif de la partie ML de ring/field	barras
2006-10-27	changement des _sym par _comm dans setoid_ring	bgregoir
2006-10-26	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin
2006-10-17	field_simplify_eq profite de la factorisation de Laurent	barras
2006-10-16	changes the use of lists and notations, to avoid that the notations	bertot
2006-10-12	Fix name clash on left	thery
2006-10-10	Remove duplicate conditions in Field + Monomial substitution function for PExpr	thery
2006-10-10	make sure BinList is not made visible to files that use the tactic Ring	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	Corrects the problem described in PR#1240:	bertot
2006-10-04	inefficacite de field_simplify_eq	barras
2006-10-02	bug dans field_simplify	barras
2006-09-29	args implicites dans Field	barras
2006-09-29	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...	barras
2006-09-28	separation de RealField	barras
2006-09-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...	barras