diff --git a/metric2/Compact.v b/metric2/Compact.v index dc6f3f6a..45315cc8 100644 --- a/metric2/Compact.v +++ b/metric2/Compact.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.model.totalorder.QposMinMax. Require Import CoRN.metric2.Limit. Require Export CoRN.metric2.FinEnum. diff --git a/metric2/FinEnum.v b/metric2/FinEnum.v index da112ace..24d97db7 100644 --- a/metric2/FinEnum.v +++ b/metric2/FinEnum.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.model.totalorder.QposMinMax. Require Export CoRN.metric2.Hausdorff. Require Import CoRN.logic.Classic. diff --git a/metric2/Limit.v b/metric2/Limit.v index 8d23bafc..461725c9 100644 --- a/metric2/Limit.v +++ b/metric2/Limit.v @@ -19,6 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.model.totalorder.QposMinMax. From Coq Require Import QArith. diff --git a/model/structures/QnonNeg.v b/model/structures/QnonNeg.v index 128d4ae6..bdb09be7 100644 --- a/model/structures/QnonNeg.v +++ b/model/structures/QnonNeg.v @@ -1,5 +1,6 @@ (* This module is designed to *not* be Import'ed, only Require'd. *) +From Coq Require Import ZArith. Require Import CoRN.model.totalorder.QposMinMax. From Coq Require Import Program. Require Import CoRN.model.structures.QposInf. diff --git a/reals/fast/CRAlternatingSum.v b/reals/fast/CRAlternatingSum.v index 1ed62b51..8eb0e06d 100644 --- a/reals/fast/CRAlternatingSum.v +++ b/reals/fast/CRAlternatingSum.v @@ -21,6 +21,7 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. From Coq Require Import ArithRing. From Coq Require Import Bool. +From Coq Require Import ZArith. From Coq Require Import Qpower Qabs. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. diff --git a/reals/fast/CRGeometricSum.v b/reals/fast/CRGeometricSum.v index df512003..60fefb11 100644 --- a/reals/fast/CRGeometricSum.v +++ b/reals/fast/CRGeometricSum.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. Require Import CoRN.reals.fast.CRAlternatingSum. @@ -1119,4 +1120,3 @@ Proof. intros. destruct (Qle_total a b). apply H, q. symmetry. apply H, q. Qed. - diff --git a/reals/fast/CRpower.v b/reals/fast/CRpower.v index 2628a700..87c49a77 100644 --- a/reals/fast/CRpower.v +++ b/reals/fast/CRpower.v @@ -19,6 +19,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.ProductMetric. @@ -27,7 +28,7 @@ From Coq Require Import Qpower. From Coq Require Import Qabs. Require Import CoRN.model.metric2.Qmetric. Require Import CoRN.model.totalorder.QMinMax. -Require Import CoRN.model.totalorder.QposMinMax. +Require Import CoRN.model.totalorder.QposMinMax. Require Import MathClasses.interfaces.canonical_names. Require Import MathClasses.interfaces.additional_operations. @@ -581,4 +582,4 @@ Proof. rewrite Nnat.nat_of_Nplus. simpl. rewrite CRpower_N_correct. reflexivity. -Qed. +Qed. diff --git a/reals/fast/CRstreams.v b/reals/fast/CRstreams.v index 95e484ea..192a90cf 100644 --- a/reals/fast/CRstreams.v +++ b/reals/fast/CRstreams.v @@ -20,9 +20,10 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.model.totalorder.QposMinMax. -Require Import CoRN.model.metric2.Qmetric. +Require Import CoRN.model.metric2.Qmetric. Require Import CoRN.metric2.Limit. From Coq Require Import Qabs. From Coq Require Import Arith. @@ -817,4 +818,3 @@ Proof. destruct q. unfold Qopp; simpl. rewrite Z.opp_involutive. reflexivity. Qed. - diff --git a/reals/fast/CRsum.v b/reals/fast/CRsum.v index cba7426d..b72ea416 100644 --- a/reals/fast/CRsum.v +++ b/reals/fast/CRsum.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. Require Import CoRN.model.totalorder.QposMinMax. diff --git a/reals/fast/Compress.v b/reals/fast/Compress.v index d27b61e8..a971d120 100644 --- a/reals/fast/Compress.v +++ b/reals/fast/Compress.v @@ -19,6 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. diff --git a/reals/fast/Interval.v b/reals/fast/Interval.v index fdc20238..db527865 100644 --- a/reals/fast/Interval.v +++ b/reals/fast/Interval.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. @@ -708,4 +709,3 @@ Proof. apply (Qle_trans _ _ _ q). apply Qlt_le_weak, ltde. Qed. - diff --git a/reals/fast/Plot.v b/reals/fast/Plot.v index d1254fb2..162c49b8 100644 --- a/reals/fast/Plot.v +++ b/reals/fast/Plot.v @@ -18,7 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) -From Coq Require Import Qround. +From Coq Require Import ZArith Qround. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.ProductMetric. Require Import CoRN.metric2.UniformContinuity. diff --git a/reals/fast/RasterQ.v b/reals/fast/RasterQ.v index 3b6d26ce..df2f70e0 100644 --- a/reals/fast/RasterQ.v +++ b/reals/fast/RasterQ.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. diff --git a/reals/fast/RasterizeQ.v b/reals/fast/RasterizeQ.v index c8e7b8e3..034fb962 100644 --- a/reals/fast/RasterizeQ.v +++ b/reals/fast/RasterizeQ.v @@ -18,6 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. diff --git a/reals/faster/ARexp.v b/reals/faster/ARexp.v index 82d61b7c..7a55ecb7 100644 --- a/reals/faster/ARexp.v +++ b/reals/faster/ARexp.v @@ -1,12 +1,13 @@ +From Coq Require Import ZArith. Require Import CoRN.algebra.RSetoid. Require Import CoRN.metric2.Metric. Require Import CoRN.metric2.UniformContinuity. From Coq Require Import Program. Require Import MathClasses.misc.workaround_tactics - CoRN.model.totalorder.QposMinMax + CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax. From Coq Require Import Qround Qabs. -Require Import CoRN.util.Qdlog CoRN.stdlib_omissions.Q +Require Import CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.fast.CRpower CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra diff --git a/reals/faster/ARsin.v b/reals/faster/ARsin.v index f590572b..bb70dedb 100644 --- a/reals/faster/ARsin.v +++ b/reals/faster/ARsin.v @@ -1,5 +1,5 @@ -From Coq Require Import Qround Qpower. -Require Import MathClasses.interfaces.abstract_algebra +From Coq Require Import ZArith Qround Qpower. +Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid @@ -8,7 +8,7 @@ Require Import MathClasses.interfaces.abstract_algebra CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog - CoRN.stdlib_omissions.Q + CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum @@ -381,4 +381,3 @@ Lemma ARtoCR_preserves_sin x : ' ucFun ARsin x = ucFun sin_slow ('x). Proof. apply preserves_unary_complete_fun. Qed. End ARsin. - diff --git a/reals/stdlib/CMTDirac.v b/reals/stdlib/CMTDirac.v index 3537e5b9..8ec13753 100644 --- a/reals/stdlib/CMTDirac.v +++ b/reals/stdlib/CMTDirac.v @@ -11,11 +11,12 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI (** Dirac measure at zero. *) -Require Import QArith. -Require Import ConstructiveReals. -Require Import ConstructiveLimits. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. +From Coq Require Import ZArith. +From Coq Require Import QArith. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveLimits. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. Require Import ConstructivePartialFunctions. Require Import CMTbase. diff --git a/reals/stdlib/CMTFullSets.v b/reals/stdlib/CMTFullSets.v index ae524078..4d6ce46d 100644 --- a/reals/stdlib/CMTFullSets.v +++ b/reals/stdlib/CMTFullSets.v @@ -13,14 +13,16 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI we now precisely define full sets, and prove that 2 functions equal on a full set have the same integral. *) -Require Import QArith. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveCauchyAbs. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveLimits. +From Coq Require Import ZArith. +From Coq Require Import QArith. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveCauchyAbs. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveLimits. + Require Import ConstructiveDiagonal. Require Import ConstructivePartialFunctions. diff --git a/reals/stdlib/CMTIntegrableFunctions.v b/reals/stdlib/CMTIntegrableFunctions.v index 82044286..2c5be33b 100644 --- a/reals/stdlib/CMTIntegrableFunctions.v +++ b/reals/stdlib/CMTIntegrableFunctions.v @@ -18,12 +18,13 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI IScomplete is complete, in the sense that its integrable functions are already integrable functions of IS : no new functions are added. *) -Require Import QArith. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveSum. -Require Import ConstructiveLimits. +From Coq Require Import ZArith. +From Coq Require Import QArith. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructiveLimits. Require Import ConstructivePartialFunctions. Require Import CMTbase. diff --git a/reals/stdlib/CMTIntegrableSets.v b/reals/stdlib/CMTIntegrableSets.v index 6f4a5e4d..23af4172 100644 --- a/reals/stdlib/CMTIntegrableSets.v +++ b/reals/stdlib/CMTIntegrableSets.v @@ -27,6 +27,7 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI *) From Coq Require Import ConstructiveEpsilon. +From Coq Require Import ZArith. From Coq Require Import QArith. From Coq Require Import ConstructiveReals. From Coq Require Import ConstructiveAbs. diff --git a/reals/stdlib/CMTMeasurableFunctions.v b/reals/stdlib/CMTMeasurableFunctions.v index 744cb1ce..8fe35e45 100644 --- a/reals/stdlib/CMTMeasurableFunctions.v +++ b/reals/stdlib/CMTMeasurableFunctions.v @@ -9,13 +9,13 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI *) -Require Import QArith. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveLimits. +From Coq Require Import ZArith QArith. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveLimits. Require Import ConstructivePartialFunctions. Require Import CMTbase. Require Import CMTIntegrableFunctions. diff --git a/reals/stdlib/CMTPositivity.v b/reals/stdlib/CMTPositivity.v index 99ddc186..fe5ad118 100644 --- a/reals/stdlib/CMTPositivity.v +++ b/reals/stdlib/CMTPositivity.v @@ -12,12 +12,13 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI (* A lemma to simplify the proofs of Icontinuous in integration spaces. It looks classical because it does not need to give a convergence modulus. *) -Require Import QArith. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveLimits. +From Coq Require Import ZArith. +From Coq Require Import QArith. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveLimits. Require Import ConstructiveDiagonal. Require Import ConstructivePartialFunctions. Require Import CMTbase. diff --git a/reals/stdlib/CMTProductIntegral.v b/reals/stdlib/CMTProductIntegral.v index c171e4e9..75bb6153 100644 --- a/reals/stdlib/CMTProductIntegral.v +++ b/reals/stdlib/CMTProductIntegral.v @@ -19,14 +19,14 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI on disjoint rectangles. Then we can take the absolute of those disjoint coefficients. *) -Require Import QArith_base. -Require Import List. -Require Import ConstructiveReals. -Require Import ConstructiveRealsMorphisms. -Require Import ConstructiveAbs. -Require Import ConstructiveSum. -Require Import ConstructiveMinMax. -Require Import ConstructiveLimits. +From Coq Require Import ZArith QArith_base. +From Coq Require Import List. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveRealsMorphisms. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveLimits. Require Import ConstructivePartialFunctions. Require Import CMTbase. Require Import CMTIntegrableFunctions. diff --git a/reals/stdlib/CMTReals.v b/reals/stdlib/CMTReals.v index e3aeb618..3805b9b0 100644 --- a/reals/stdlib/CMTReals.v +++ b/reals/stdlib/CMTReals.v @@ -29,14 +29,14 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI of the values of the functions with zero. *) -Require Import QArith Qminmax Qpower Qabs. - -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveLimits. +From Coq Require Import ZArith QArith Qminmax Qpower Qabs. + +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveLimits. Require Import ConstructiveDiagonal. Require Import ConstructivePartialFunctions. Require Import ConstructiveUniformCont. diff --git a/reals/stdlib/CMTprofile.v b/reals/stdlib/CMTprofile.v index 4ee62404..bc53b062 100644 --- a/reals/stdlib/CMTprofile.v +++ b/reals/stdlib/CMTprofile.v @@ -25,13 +25,13 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI prove that this non-increasing limit of integrals exists. *) -Require Import QArith_base Qabs. -Require Import ConstructiveReals. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveLimits. +From Coq Require Import ZArith QArith_base Qabs. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveLimits. Require Import ConstructiveUniformCont. Require Import ConstructivePartialFunctions. Require Import ConstructiveDiagonal. @@ -40,7 +40,7 @@ Require Import CMTIntegrableFunctions. Require Import CMTIntegrableSets. Require Import CMTFullSets. Require Import CMTReals. -Require Import Lia. +From Coq Require Import Lia. Local Open Scope ConstructiveReals. diff --git a/reals/stdlib/ConstructiveCauchyIntegral.v b/reals/stdlib/ConstructiveCauchyIntegral.v index 7315844c..59f1b3b2 100644 --- a/reals/stdlib/ConstructiveCauchyIntegral.v +++ b/reals/stdlib/ConstructiveCauchyIntegral.v @@ -21,14 +21,14 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI functions. *) -Require Import List Permutation Orders Sorted Mergesort. -Require Import QArith Qpower. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveSum. -Require Import ConstructiveLimits. -Require Import ConstructiveRcomplete. +From Coq Require Import List Permutation Orders Sorted Mergesort. +From Coq Require Import ZArith QArith Qpower. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructiveLimits. +From Coq Require Import ConstructiveRcomplete. Require Import ConstructiveDiagonal. Require Import ConstructiveUniformCont. diff --git a/reals/stdlib/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v index 840c8dcb..df1b0695 100644 --- a/reals/stdlib/ConstructiveDiagonal.v +++ b/reals/stdlib/ConstructiveDiagonal.v @@ -12,14 +12,15 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI (* The diagonal bijection between nat^2 and nat, as well as convergence results for double series. *) -Require Import QArith. -Require Import PeanoNat. -Require Import ArithRing. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveLimits. +From Coq Require Import ZArith. +From Coq Require Import QArith. +From Coq Require Import PeanoNat. +From Coq Require Import ArithRing. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveLimits. Local Open Scope ConstructiveReals. diff --git a/reals/stdlib/ConstructiveFastReals.v b/reals/stdlib/ConstructiveFastReals.v index 0beff6c9..d0a6bb2e 100644 --- a/reals/stdlib/ConstructiveFastReals.v +++ b/reals/stdlib/ConstructiveFastReals.v @@ -12,7 +12,7 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI (** Proof that CoRN's fast reals implement the standard library's interface ConstructiveReals. *) -From Coq Require Import ConstructiveReals. +From Coq Require Import ZArith ConstructiveReals. Require Import CoRN.model.metric2.Qmetric. Require Import CoRN.model.metric2.CRmetric. Require Import CoRN.reals.fast.CRFieldOps. @@ -372,4 +372,3 @@ Definition FastRealsConstructive : ConstructiveReals CRmult_inv_r_nlt CRinv_0_lt_compat CRlt_Qmid CRup CRabs CRabs_nlt CRcauchy_complete. - diff --git a/reals/stdlib/ConstructivePartialFunctions.v b/reals/stdlib/ConstructivePartialFunctions.v index 1ba4f0f6..47533783 100644 --- a/reals/stdlib/ConstructivePartialFunctions.v +++ b/reals/stdlib/ConstructivePartialFunctions.v @@ -15,14 +15,15 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI definition which are subsets of X. *) -Require Import List. -Require Import QArith. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveSum. -Require Import ConstructiveLimits. -Require Import ConstructiveRcomplete. +From Coq Require Import List. +From Coq Require Import ZArith. +From Coq Require Import QArith. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructiveLimits. +From Coq Require Import ConstructiveRcomplete. Local Open Scope ConstructiveReals. @@ -858,4 +859,3 @@ Proof. (fun x y => let (xD,xnz) := y in CRinv R (partialApply f x xD) xnz)). intros. destruct p,q. apply CRinv_morph, DomainProp. Defined. - diff --git a/reals/stdlib/ConstructiveUniformCont.v b/reals/stdlib/ConstructiveUniformCont.v index 942aced1..36a19966 100644 --- a/reals/stdlib/ConstructiveUniformCont.v +++ b/reals/stdlib/ConstructiveUniformCont.v @@ -14,14 +14,14 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI The uniformly continuous functions R -> R. *) -Require Import List Permutation Orders Sorted Mergesort. -Require Import QArith Qpower. -Require Import ConstructiveReals. -Require Import ConstructiveAbs. -Require Import ConstructiveMinMax. -Require Import ConstructiveSum. -Require Import ConstructivePower. -Require Import ConstructiveLimits. +From Coq Require Import List Permutation Orders Sorted Mergesort. +From Coq Require Import ZArith QArith Qpower. +From Coq Require Import ConstructiveReals. +From Coq Require Import ConstructiveAbs. +From Coq Require Import ConstructiveMinMax. +From Coq Require Import ConstructiveSum. +From Coq Require Import ConstructivePower. +From Coq Require Import ConstructiveLimits. Require Import ConstructiveDiagonal. Local Open Scope ConstructiveReals. diff --git a/util/Qsums.v b/util/Qsums.v index ac2e4383..d50f7ce6 100644 --- a/util/Qsums.v +++ b/util/Qsums.v @@ -1,3 +1,4 @@ +From Coq Require Import ZArith. Require Import CoRN.stdlib_omissions.List. From Coq Require Import QArith Qabs. Require Import CoRN.model.totalorder.QposMinMax