aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
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
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2677 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-06Cosmétiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2668 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-06Standardisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2667 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-19lemmes sur Zdiv/Zmodfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2661 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique ↵filliatr
FourierR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2659 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17*** empty log message ***werner
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2656 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Quelques bugs avec inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08Zdiv -> Export ZArithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2621 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-08syntaxe pour Zdiv et Zmodfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2620 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05simplification preuvefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2615 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05nouveau module Zdivfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2614 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02Optimisationdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2582 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02Suppression PI_lb et PI_ubdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2581 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-02Suppression Fielddesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2580 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-29sans utiliser Fielddesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2578 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-29Suppression des invocations a Fielddesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2575 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-26Prise en compte des dependances dans la tactique Casemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-22*** empty log message ***werner
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2566 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de ↵herbelin
Zsyntax et de Rsyntax (dont les règles ne s'appliquent plus dans le même ordre depuis la modification de l'ordre de chargement des Require) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2564 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
soi-même si nécessaire) : l'idée est d'avoir un comportement clair et toujours aussi rapide que possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2559 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-02 20:31:10 +0000