aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-07-16R_sqr ne contient plus de resultats sur sqrt -> R_sqrtdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2878 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Realsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2877 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Rgeomdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2876 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Proprietes (calculatoires) des fonctions trigonometriquesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Proprietes de la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2874 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Definition de la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2873 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15code retour de make checkcourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2872 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Pb de factorisation camlp4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2871 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Pour assurer une compatibilite avec la 7.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2870 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Bug de précédenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitcourant
de la forme (E->F)->G. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Preuve de cos_plusdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2863 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Quelques resultats supplementaires sur les suites convergentesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2862 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Le theoreme central sur les produits de Cauchy finisdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2861 85f007b7-540e-0410-9357-904b9bb8a0f7
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-12*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2859 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-11Protection contre l'encapsulage de FailError dans Exc_located (sinon, par ↵herbelin
exemple, 'Try Tauto' ne marche pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2855 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Error_in_file redondant et inappropriéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2854 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Que la localisation des erreurs pour les tactiques atomiques marcheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2853 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourherbelin
les définitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:20:34 +0000