coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-05	sin_bound et cos_bound sont prouves (merci les series alternees...)	desmettr
2002-07-03	* empty log message *	desmettr
2002-07-03	sin_eq_0 est maintenant prouve	desmettr
2002-07-02	sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)	desmettr
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-01	Constructions des séries alternées et de PI	desmettr
2002-07-01	PI n'est plus un axiome	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-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-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-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-11	* empty log message *	desmettr
2002-06-11	Ranalysis.v	desmettr
2002-06-06	Correction non reconnaissance des variables de section dans les afficheurs de...	herbelin
2002-05-31	Ajout d'occurrences de Field (ne pas enlever)	delahaye
2002-05-29	Double Induction prend maintenant des noms d'hyppthèses	herbelin
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-04-02	Optimisation	desmettr
2002-04-02	Suppression PI_lb et PI_ub	desmettr
2002-04-02	Suppression Field	desmettr
2002-03-29	sans utiliser Field	desmettr
2002-03-29	Suppression des invocations a Field	desmettr
2002-03-22	Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...	herbelin
2002-03-21	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant
2002-03-20	Intuition now takes an (optional) tactic as parameter. This tactic is	courant
2002-03-19	Exportation de SplitRmult et SplitAbsolu	delahaye
2002-03-17	Field ne fait maintenant que les reductions necessaires	delahaye
2002-03-07	* empty log message *	desmettr
2002-02-14	option -dump-glob pour coqdoc	filliatr
2002-01-07	Ajout en-tête	herbelin
2001-12-21	Passage coqweb	herbelin
2001-12-19	* empty log message *	desmettr
2001-12-07	* empty log message *	desmettr
2001-12-07	* empty log message *	desmettr
2001-12-05	* empty log message *	desmettr
2001-12-05	* empty log message *	desmettr
2001-12-05	* empty log message *	desmettr