aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-07-09Making the sumbool functions transparent, so that they can used tobertot
compute even inside Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05certains lemmes sont maintenant dans Rtrigodesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2844 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05sin_plus prouve (a partir de cos_plus)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2843 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05sin_bound et cos_bound deplaces dans Rtrigo_altdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2842 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05sin_bound et cos_bound sont prouves (merci les series alternees...)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2841 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2840 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05*** empty log message ***corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2839 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05Added a new uncompleteness bug found in Tauto.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2838 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03Hack pour autoriser les $n dans les Grammar tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2837 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2836 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03sin_eq_0 est maintenant prouvedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2835 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2830 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02reparation pretyping ROldCase dans le cas letfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2829 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02factorisation code dans make_dep_of_undepfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2827 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2826 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02Suppression de l'axiome arc_sin_cosdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2823 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02Modification de IAF, introduction de TAF et preuves de 3 axiomesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2822 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2821 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Constructions des séries alternées et de PIdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2819 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01PI n'est plus un axiomedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2818 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2817 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2816 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Version plus propre de Rsigmadesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2815 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Ajout de Binomedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2814 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Formule du binome (pour cos(x+y), sin(x+y)...)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2813 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Modification sin_approxdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2812 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-28resynchronisation du .depend.coqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2810 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-26*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2809 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-26*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2808 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-26Resolution de bug (du a Auto; remplacement par lt_O_Sn)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2807 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-25Integration de Rcomplet et Alembert_compldesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2806 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-25Integration de Rcomplet et Alembert_compldesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2805 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-25*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2804 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-21Suppression de l'axiome d'extensionnalitedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2803 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20Nouvelle version avec INR + Amelioration de Sup0.mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2801 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2800 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2799 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-19Reparation de ring pour les setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2797 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-19ProgWf -> Zwffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2796 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-19Coercion de la syntaxe des motifs non atomiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2794 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-18coq_makefile utilise maintenant coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2793 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17Suppression de fct_eqdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2792 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17Prise en compte de exp, cosh et sinhdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2791 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17Modifications relatives a l'ajout de Rtrigo_defdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2790 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17Definitions de exp, cos et sindesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2789 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2788 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-14*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2787 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-22 00:21:53 +0000