diff options
author | 2006-09-26 12:13:06 +0000 | |
---|---|---|
committer | 2006-09-26 12:13:06 +0000 | |
commit | 4aec8fda1161953cf929b4e282eea9b672ab4058 (patch) | |
tree | eea4b8ab24fdea8fb05206b1764ce1ed3c752d72 /theories/Reals | |
parent | 351a500eada776832ac9b09657e42f5d6cd7210f (diff) |
commit de field + renommages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
-rw-r--r-- | theories/Reals/ArithProp.v | 2 | ||||
-rw-r--r-- | theories/Reals/RIneq.v | 13 | ||||
-rw-r--r-- | theories/Reals/Rfunctions.v | 4 |
3 files changed, 10 insertions, 9 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index c05ea465d..a00d42879 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rbasic_fun. Require Import Even. Require Import Div2. -Require Import NewArithRing. +Require Import ArithRing. Open Local Scope Z_scope. Open Local Scope R_scope. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 3b5d241fa..c6feb4ac6 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -13,9 +13,9 @@ (***************************************************************************) Require Export Raxioms. -Require Export NewZArithRing. +Require Export ZArithRing. Require Import Omega. -Require Export Field_tac. Import NewField. +Require Export Field_tac. Import Field. Open Local Scope Z_scope. Open Local Scope R_scope. @@ -88,7 +88,7 @@ apply Rlt_trans with (0 + 1). apply Rplus_0_l. Qed. -Lemma Rgen_phiPOS : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x > 0. +Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0. unfold Rgt in |- *. induction x; simpl in |- *; intros. apply Rlt_trans with (1 + 0). @@ -111,7 +111,8 @@ induction x; simpl in |- *; intros. Qed. -Lemma Rgen_phiPOS_not_0 : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x <> 0. +Lemma Rgen_phiPOS_not_0 : + forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0. red in |- *; intros. specialize (Rgen_phiPOS x). rewrite H in |- *; intro. @@ -119,8 +120,8 @@ apply (Rlt_asym 0 0); trivial. Qed. Lemma Zeq_bool_complete : forall x y, - ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = - ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> Zeq_bool x y = true. Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 878d5f73d..99c804272 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -15,8 +15,8 @@ (** Definition of the sum functions *) (* *) (********************************************************) -Require Export ArithRing. (* for ring_nat... *) -Require Export NewArithRing. +Require Export LegacyArithRing. (* for ring_nat... *) +Require Export ArithRing. Require Import Rbase. Require Export R_Ifp. |