coq - The formal proof system

Age	Commit message (Expand)	Author
2006-11-16	suppression de code mort (avec bug de nom)	letouzey
2006-11-16	pb avec r9379 + modifs dans ring	barras
2006-11-16	Work on dep types pattern matching	msozeau
2006-11-16	suite de r9362: reconnaissance de qqs injections entre nat, N et Z	barras
2006-11-15	Some usability enhancements.	msozeau
2006-11-13	Better solve using tactics impl.	msozeau
2006-11-13	Correction de la seconde partie du bug #1278	jforest
2006-11-13	Correction de la premiere partie du #1278 (but non referme en cas d'echec)	jforest
2006-11-13	Encore des _sym au lieu de _comm	herbelin
2006-11-10	generalisation de ring pour faire Ring_nf	barras
2006-11-10	Work on mutual defs, various bug fixes.	msozeau
2006-11-10	Work on pattern inequalities for pattern matching branches.	msozeau
2006-11-09	Support for mutual defs in obligation handling.	msozeau
2006-10-31	Debug obligation handling code	msozeau
2006-10-31	Fix compile error	msozeau
2006-10-31	Work on obligation separation.	msozeau
2006-10-30	fixed field_simplify + changed precedence of let and fun in ltac	barras
2006-10-29	Suite commit polymorphisme	herbelin
2006-10-29	Exports manquants dans ring	barras
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-28	Fixes in experimental merging of functional graphs.	courtieu
2006-10-27	simplif de la partie ML de ring/field	barras
2006-10-27	Fixes on functional graphs merging: put functional results at the end	courtieu
2006-10-27	changement des _sym par _comm dans setoid_ring	bgregoir
2006-10-27	Fixes on functional graphs merging: removed debug printing.	courtieu
2006-10-27	Fixes on functional graphs merging: names of constructors.	courtieu
2006-10-26	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin
2006-10-26	Noms de compatibilité déplacés en bloc à la fin du fichier	herbelin
2006-10-26	Some fixes in experimental merging of two functional graphs.	courtieu
2006-10-26	Experimental merging of two functional graphs.	courtieu
2006-10-26	Facilities to automatically solve obligations	msozeau
2006-10-25	Ménage	notin
2006-10-25	oops	barras
2006-10-25	conflit de nom (Field_theory) modulo la casse	barras
2006-10-24	Extension de fresh (suite)	herbelin
2006-10-20	Starting to add a function schemes merging command (not finished, not	courtieu
2006-10-19	Correction sym -> comm	herbelin
2006-10-17	field_simplify_eq profite de la factorisation de Laurent	barras
2006-10-16	affichage des ... dans les scripts	barras
2006-10-16	typo doc + bug legacy field	barras
2006-10-16	changes the use of lists and notations, to avoid that the notations	bertot
2006-10-13	r9778@tannat: jforest \| 2006-10-13 11:36:37 +0200	jforest
2006-10-12	Fix name clash on left	thery
2006-10-10	Fix 0 obligations bug	msozeau
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-09	Notations:	herbelin
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