coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-01	Constructions des séries alternées et de PI	desmettr
2002-07-01	PI n'est plus un axiome	desmettr
2002-07-01	* empty log message *	desmettr
2002-07-01	* empty log message *	desmettr
2002-07-01	Version plus propre de Rsigma	desmettr
2002-07-01	Ajout de Binome	desmettr
2002-07-01	Formule du binome (pour cos(x+y), sin(x+y)...)	desmettr
2002-07-01	Modification sin_approx	desmettr
2002-06-28	resynchronisation du .depend.coq	letouzey
2002-06-26	* empty log message *	mohring
2002-06-26	* empty log message *	mohring
2002-06-26	Resolution de bug (du a Auto; remplacement par lt_O_Sn)	mayero
2002-06-25	Integration de Rcomplet et Alembert_compl	desmettr
2002-06-25	Integration de Rcomplet et Alembert_compl	desmettr
2002-06-25	* empty log message *	desmettr
2002-06-21	Suppression de l'axiome d'extensionnalite	desmettr
2002-06-21	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr
2002-06-20	Nouvelle version avec INR + Amelioration de Sup0.	mayero
2002-06-20	* empty log message *	desmettr
2002-06-20	maj	filliatr
2002-06-20	ZArith_base, Zbool, Bool_nat	filliatr
2002-06-19	Reparation de ring pour les setoides	clrenard
2002-06-19	ProgWf -> Zwf	filliatr
2002-06-19	deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf	filliatr
2002-06-19	Coercion de la syntaxe des motifs non atomiques	herbelin
2002-06-18	coq_makefile utilise maintenant coqdoc	filliatr
2002-06-17	Suppression de fct_eq	desmettr
2002-06-17	Prise en compte de exp, cosh et sinh	desmettr
2002-06-17	Modifications relatives a l'ajout de Rtrigo_def	desmettr
2002-06-17	Definitions de exp, cos et sin	desmettr
2002-06-17	* empty log message *	desmettr
2002-06-14	* empty log message *	herbelin
2002-06-14	Commentaires	herbelin
2002-06-14	* empty log message *	herbelin
2002-06-13	Bug non vérification non redondance par Cut	herbelin
2002-06-13	Nouvelle version de l'algorithme de compilation du filtrage compatible avec u...	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin
2002-06-13	Ajout map_inductive_type et map_ind_family	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context	herbelin
2002-06-13	Réparation de l'interprétation des fermetures (sans casser Field!)	herbelin
2002-06-13	Petits beug d'affichages.	gregoire
2002-06-11	Tests pour la tactique Reg	desmettr
2002-06-11	* empty log message *	desmettr
2002-06-11	* empty log message *	desmettr
2002-06-11	Ranalysis.v	desmettr
2002-06-07	L'ordre supérieur avait quelque peu été oublié dans l'unification...	herbelin
2002-06-07	extraction vers scheme	letouzey
2002-06-07	Adding file theories/ZArith/Zsqrt.v that contains a square root function.	bertot
2002-06-07	Ajout de FNL ou utilisation de msgnl	herbelin
2002-06-07	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin