aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2002-07-12Differents resultats sur les produits finisdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2860 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12cos_plus prouvedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2858 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Hack pour parser '{x:T|P}*B' sans parenthesesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2857 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-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-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-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-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-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-11*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2776 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11Ranalysis.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2774 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
actually three functions are provided, one working on positive numbers (it is structurally recursive), one with a strong specification (Zsqrt), and one with a weak specification (Zsqrt_plain). For the function with a weak specification an extra theorem is also provided. The decision functions in ZArith_dec have been made transparent so that computation with the square root function also becomes possible with Lazy Beta Iota Delta Zeta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs ↵herbelin
de Z et R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2760 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2758 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-31Ajout d'occurrences de Field (ne pas enlever)delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2742 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2731 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Introduction de syntaxe convivial +,*,<=,<,>=herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2730 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Double Induction prend maintenant des noms d'hyppthèsesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2729 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2728 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Contournement des My_special_variableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2727 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2712 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16Ajout Peano_dec et Compare_decherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2698 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2697 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14petite erreur de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2683 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14encore des lemmes sur Zdivfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2678 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 15:24:50 +0000