Merge pull request #214 from coq-community/coq_19801

Adapt to rocq-prover/rocq#19801

Author: proux01

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.