Merge pull request #214 from coq-community/coq_19801

Adapt to coq/coq#19801

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.

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.

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.

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.

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.

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.
-

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.

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.
-

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.

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.

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.
-

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.

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.

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.

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 

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.
-

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.
 

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.
 

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.
 

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.

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.

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.

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.

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.

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.
 

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.