| Age | Commit message (Expand) | Author |
| 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-09 | Making the sumbool functions transparent, so that they can used to | bertot |
| 2002-07-05 | 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-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 |