coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	* 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-07-01
*	resynchronisation du .depend.coq	letouzey	2002-06-28
*	* 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-26
*	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-25
*	Suppression de l'axiome d'extensionnalite	desmettr	2002-06-21
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
*	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-20
*	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-19
*	coq_makefile utilise maintenant coqdoc	filliatr	2002-06-18
*	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-17
*	* empty log message *	herbelin	2002-06-14
*	Commentaires	herbelin	2002-06-14
*	* empty log message *	herbelin	2002-06-14
*	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-13
*	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-11
*	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	2002-06-07
*	I added a comment on the tactic compute_POS.	bertot	2002-06-07
*	This example does not work in coq-7.3, but does in coq-7.2.	bertot	2002-06-07
*	Ajout coercion constr vers hyp quantifiée	herbelin	2002-06-06