coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bug de précédence	herbelin	2002-07-15
*	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant	2002-07-15
*	Preuve de cos_plus	desmettr	2002-07-12
*	Quelques resultats supplementaires sur les suites convergentes	desmettr	2002-07-12
*	Le theoreme central sur les produits de Cauchy finis	desmettr	2002-07-12
*	Differents resultats sur les produits finis	desmettr	2002-07-12
*	* empty log message *	desmettr	2002-07-12
*	cos_plus prouve	desmettr	2002-07-12
*	Hack pour parser '{x:T\|P}*B' sans parentheses	herbelin	2002-07-11
*	Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...	herbelin	2002-07-11
*	Error_in_file redondant et inapproprié	herbelin	2002-07-11
*	Que la localisation des erreurs pour les tactiques atomiques marche	herbelin	2002-07-11
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Making the sumbool functions transparent, so that they can used to	bertot	2002-07-09
*	certains lemmes sont maintenant dans Rtrigo	desmettr	2002-07-05
*	sin_plus prouve (a partir de cos_plus)	desmettr	2002-07-05
*	sin_bound et cos_bound deplaces dans Rtrigo_alt	desmettr	2002-07-05
*	sin_bound et cos_bound sont prouves (merci les series alternees...)	desmettr	2002-07-05
*	* empty log message *	desmettr	2002-07-05
*	* empty log message *	corbinea	2002-07-05
*	Added a new uncompleteness bug found in Tauto.	corbinea	2002-07-05
*	Hack pour autoriser les $n dans les Grammar tactic	herbelin	2002-07-03
*	* empty log message *	desmettr	2002-07-03
*	sin_eq_0 est maintenant prouve	desmettr	2002-07-03
*	sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)	desmettr	2002-07-02
*	reparation pretyping ROldCase dans le cas let	filliatr	2002-07-02
*	factorisation code dans make_dep_of_undep	filliatr	2002-07-02
*	maj	filliatr	2002-07-02
*	Suppression de l'axiome arc_sin_cos	desmettr	2002-07-02
*	Modification de IAF, introduction de TAF et preuves de 3 axiomes	desmettr	2002-07-02
*	* empty log message *	desmettr	2002-07-02
*	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-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