coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-05	Added a new uncompleteness bug found in Tauto.	corbinea
2002-07-03	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-02	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-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