aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/ZArith_dec.v2
-rw-r--r--theories/ZArith/Zbool.v2
-rw-r--r--theories/ZArith/Zcomplements.v2
-rw-r--r--theories/ZArith/Zmisc.v2
-rw-r--r--theories/ZArith/Zsqrt_compat.v2
-rw-r--r--theories/ZArith/Zwf.v2
6 files changed, 6 insertions, 6 deletions
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index cac3cd4e5..8d535d509 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -11,7 +11,7 @@ Require Import Sumbool.
Require Import BinInt.
Require Import Zorder.
Require Import Zcompare.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(* begin hide *)
(* Trivial, to deprecate? *)
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 3a86a821b..a38974339 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -13,7 +13,7 @@ Require Import Zcompare.
Require Import ZArith_dec.
Require Import Sumbool.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(** * Boolean operations from decidability of order *)
(** The decidability of equality and order relations over
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index dde0745eb..7ae2a67ca 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -10,7 +10,7 @@ Require Import ZArithRing.
Require Import ZArith_base.
Require Export Omega.
Require Import Wf_nat.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(**********************************************************************)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index bfd57d758..b871f9c98 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -11,7 +11,7 @@ Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
Require Import Bool.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(**********************************************************************)
(** Iterators *)
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index 54f6f2e9a..0a5ad4ace 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -9,7 +9,7 @@
Require Import ZArithRing.
Require Import Omega.
Require Export ZArith_base.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(** THIS FILE IS DEPRECATED
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index efe5b6847..0a4418671 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -9,7 +9,7 @@
Require Import ZArith_base.
Require Export Wf_nat.
Require Import Omega.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
(** Well-founded relations on Z. *)