aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--theories/Reals/Alembert.v3
-rw-r--r--theories/Reals/AltSeries.v3
-rw-r--r--theories/Reals/ArithProp.v3
-rw-r--r--theories/Reals/Binomial.v3
-rw-r--r--theories/Reals/Cauchy_prod.v3
-rw-r--r--theories/Reals/Cos_rel.v3
-rw-r--r--theories/Reals/PartSum.v3
-rw-r--r--theories/Reals/RList.v3
-rw-r--r--theories/Reals/R_Ifp.v2
-rw-r--r--theories/Reals/Rcomplete.v3
-rw-r--r--theories/Reals/Rfunctions.v9
-rw-r--r--theories/Reals/RiemannInt_SF.v3
-rw-r--r--theories/Reals/Rprod.v3
-rw-r--r--theories/Reals/Rseries.v2
-rw-r--r--theories/Reals/Rsigma.v3
-rw-r--r--theories/Reals/Rsqrt_def.v3
-rw-r--r--theories/Reals/Rtrigo.v3
-rw-r--r--theories/Reals/Rtrigo_alt.v3
-rw-r--r--theories/Reals/Rtrigo_calc.v3
-rw-r--r--theories/Reals/Rtrigo_def.v3
-rw-r--r--theories/Reals/Rtrigo_fun.v2
-rw-r--r--theories/Reals/Rtrigo_reg.v3
-rw-r--r--theories/Reals/SeqProp.v3
-rw-r--r--theories/Reals/SeqSeries.v5
24 files changed, 45 insertions, 32 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 6745a3fc4..acc0c7afc 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -14,7 +14,8 @@ Require Rseries.
Require SeqProp.
Require PartSum.
Require Max.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(***************************************************)
(* Various versions of the criterion of D'Alembert *)
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index b512f9bea..c35f18a73 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -14,7 +14,8 @@ Require Rseries.
Require SeqProp.
Require PartSum.
Require Max.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(**********)
Definition tg_alt [Un:nat->R] : nat->R := [i:nat]``(pow (-1) i)*(Un i)``.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index db4494dd2..7ec8ad1ed 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,8 +12,9 @@ Require Rbase.
Require Rbasic_fun.
Require Even.
Require Div2.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
Open Local Scope Z_scope.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Open Local Scope R_scope.
Lemma minus_neq_O : (n,i:nat) (lt i n) -> ~(minus n i)=O.
Intros; Red; Intro.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 1751f8277..5bbf8c7dd 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -11,7 +11,8 @@
Require Rbase.
Require Rfunctions.
Require PartSum.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Definition C [n,p:nat] : R := ``(INR (fact n))/((INR (fact p))*(INR (fact (minus n p))))``.
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index 697316b84..a76307320 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -12,7 +12,8 @@ Require Rbase.
Require Rfunctions.
Require Rseries.
Require PartSum.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(**********)
Lemma sum_N_predN : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==``(sum_f_R0 An (pred N)) + (An N)``.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index c59c00e08..0bc58169c 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -12,7 +12,8 @@ Require Rbase.
Require Rfunctions.
Require SeqSeries.
Require Rtrigo_def.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Definition A1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))*(pow x (mult (S (S O)) k))`` N).
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 9db2ebc66..090680cf1 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -13,7 +13,8 @@ Require Rfunctions.
Require Rseries.
Require Rcomplete.
Require Max.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``.
Intros; Induction N.
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 3cccc2bfc..6e6f2716b 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -10,7 +10,8 @@
Require Rbase.
Require Rfunctions.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Inductive Rlist : Type :=
| nil : Rlist
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 81baa6c29..b167b6ef9 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -15,7 +15,7 @@
Require Rbase.
Require Omega.
-
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
Open Local Scope R_scope.
(*********************************************************)
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index edcddeb25..5dca3068c 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -13,7 +13,8 @@ Require Rfunctions.
Require Rseries.
Require SeqProp.
Require Max.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(****************************************************)
(* R is complete : *)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 31c3e13ea..3ea74f862 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -25,9 +25,8 @@ Require Export SplitRmult.
Require Export ArithProp.
Require Omega.
Require Zpower.
-V7only [Import nat_scope.].
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
Open Local Scope nat_scope.
-V7only [Import R_scope.].
Open Local Scope R_scope.
(*******************************)
@@ -68,8 +67,6 @@ Fixpoint pow [r:R;n:nat]:R:=
|(S n) => (Rmult r (pow r n))
end.
-Arguments Scope pow [ R_scope nat_scope ].
-
Lemma pow_O: (e : R) (pow e O) == R1.
Simpl; Auto with real.
Qed.
@@ -675,14 +672,10 @@ Fixpoint sum_f_R0 [f:nat->R;N:nat]:R:=
|(S i) => (Rplus (sum_f_R0 f i) (f (S i)))
end.
-Arguments Scope sum_f_R0 [ _ nat_scope ].
-
(*********)
Definition sum_f [s,n:nat;f:nat->R]:R:=
(sum_f_R0 [x:nat](f (plus x s)) (minus n s)).
-Arguments Scope sum_f [ nat_scope nat_scope _ ].
-
Lemma GP_finite:
(x:R) (n:nat) (Rmult (sum_f_R0 [n:nat] (pow x n) n)
(Rminus x R1)) ==
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 1fc9811e5..f81c57997 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -12,7 +12,8 @@ Require Rbase.
Require Rfunctions.
Require Ranalysis.
Require Classical_Prop.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Implicit Arguments On.
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 0093eb15e..c613c7647 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -14,7 +14,8 @@ Require Rfunctions.
Require Rseries.
Require PartSum.
Require Binomial.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(* TT Ak; 1<=k<=N *)
Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index f7f8cdddb..032524771 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -12,6 +12,8 @@ Require Rbase.
Require Rfunctions.
Require Classical.
Require Compare.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Implicit Variable Type r:R.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 445343f7a..fd14d2c8c 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -12,7 +12,8 @@ Require Rbase.
Require Rfunctions.
Require Rseries.
Require PartSum.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Set Implicit Arguments.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 94917e42a..ebdece374 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -13,7 +13,8 @@ Require Rbase.
Require Rfunctions.
Require SeqSeries.
Require Ranalysis1.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R :=
Cases N of
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 2696b0453..ae23fd8a6 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -19,9 +19,8 @@ Require Export Cos_plus.
Require ZArith_base.
Require Zcomplements.
Require Classical_Prop.
-V7only [Import nat_scope.].
+V7only [Import nat_scope. Import Z_scope. Import R_scope.].
Open Local Scope nat_scope.
-V7only [Import R_scope.].
Open Local Scope R_scope.
(** sin_PI2 is the only remaining axiom **)
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 7e8ef465b..4fdc39106 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -12,7 +12,8 @@ Require Rbase.
Require Rfunctions.
Require SeqSeries.
Require Rtrigo_def.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(*****************************************************************)
(* Using series definitions of cos and sin *)
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index f5e3912bf..8ede9fc1c 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -13,7 +13,8 @@ Require Rfunctions.
Require SeqSeries.
Require Rtrigo.
Require R_sqrt.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Lemma tan_PI : ``(tan PI)==0``.
Unfold tan; Rewrite sin_PI; Rewrite cos_PI; Unfold Rdiv; Apply Rmult_Ol.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index de7a49568..82c63a7b2 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -13,7 +13,8 @@ Require Rfunctions.
Require SeqSeries.
Require Rtrigo_fun.
Require Max.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(*****************************)
(* Definition of exponential *)
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index b0ccff5d2..33c3f6a5f 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -11,6 +11,8 @@
Require Rbase.
Require Rfunctions.
Require SeqSeries.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(*****************************************************************)
(* To define transcendental functions *)
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 1808e1a5a..1155a05a0 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -14,9 +14,8 @@ Require SeqSeries.
Require Rtrigo.
Require Ranalysis1.
Require PSeries_reg.
-V7only [Import nat_scope.].
+V7only [Import nat_scope. Import Z_scope. Import R_scope.].
Open Local Scope nat_scope.
-V7only [Import R_scope.].
Open Local Scope R_scope.
Lemma CVN_R_cos : (fn:nat->R->R) (fn == [N:nat][x:R]``(pow (-1) N)/(INR (fact (mult (S (S O)) N)))*(pow x (mult (S (S O)) N))``) -> (CVN_R fn).
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 5961ab832..913dfd69a 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -13,7 +13,8 @@ Require Rfunctions.
Require Rseries.
Require Classical.
Require Max.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)).
Definition opp_seq [Un:nat->R] : nat->R := [n:nat]``-(Un n)``.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 088a9280e..03963fc4d 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -21,7 +21,8 @@ Require Export Rsigma.
Require Export Rprod.
Require Export Cauchy_prod.
Require Export Alembert.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Open Local Scope R_scope.
(**********)
Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``.
@@ -303,4 +304,4 @@ Apply sum_eq; Intros; Ring.
Apply H5; Unfold ge; Apply le_S_n; Replace (S (pred n)) with n.
Apply S_pred with O; Apply lt_le_trans with (S x).
Apply lt_O_Sn.
-Qed. \ No newline at end of file
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 10:09:32 +0000