diff options
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zmisc.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zsqrt.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zwf.v | 1 |
9 files changed, 9 insertions, 1 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index d02c46e082..035e16f220 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -13,6 +13,7 @@ Require zarith_aux. Require auxiliary. Require Zsyntax. V7only [Import Z_scope.]. +Open Local Scope Z_scope. (** Our purpose is to write an induction shema for {0,1,2,...} similar to the [nat] schema (Theorem [Natlike_rec]). For that the diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 98c1dc32f9..88e7c325d7 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -15,7 +15,7 @@ Require zarith_aux. Require auxiliary. Require Zsyntax. V7only [Import Z_scope.]. - +Open Local Scope Z_scope. Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}. Proof. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 34971439b3..954347d89d 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -13,6 +13,7 @@ Require ZArithRing. Require Omega. Require Wf_nat. V7only [Import Z_scope.]. +Open Local Scope Z_scope. (** Multiplication by a number >0 preserves [Zcompare]. It also perserves [Zle], [Zlt], [Zge], [Zgt] *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index ce1bd0335b..e888d87d03 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -24,6 +24,7 @@ Require Omega. Require ZArithRing. Require Zcomplements. V7only [Import Z_scope.]. +Open Local Scope Z_scope. (** diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index aa97d4bf87..0fe380e718 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -24,6 +24,7 @@ Require Omega. Require Zcomplements. Require Zpower. V7only [Import Z_scope.]. +Open Local Scope Z_scope. Section Log_pos. (* Log of positive integers *) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 3e2d8a4aae..8a7a1caa44 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -14,6 +14,7 @@ Require auxiliary. Require Zsyntax. Require Bool. V7only [Import Z_scope.]. +Open Local Scope Z_scope. (** Overview of the sections of this file: - logic: Logic complements. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 4dbfa8fc8a..8f695a166f 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -12,6 +12,7 @@ Require ZArith_base. Require Omega. Require Zcomplements. V7only [Import Z_scope.]. +Open Local Scope Z_scope. Section section1. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 681dcdd122..3c895d6dba 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -12,6 +12,7 @@ Require Export ZArith_base. Require Export ZArithRing. Require Export Omega. V7only [Import Z_scope.]. +Open Local Scope Z_scope. (** The following tactic replaces all instances of (POS (xI ...)) by `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *) diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 569be3b313..5468f82cc8 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -12,6 +12,7 @@ Require ZArith_base. Require Export Wf_nat. Require Omega. V7only [Import Z_scope.]. +Open Local Scope Z_scope. (** Well-founded relations on Z. *) |