aboutsummaryrefslogtreecommitdiff
path: root/contrib7
diff options
context:
space:
mode:
Diffstat (limited to 'contrib7')
-rw-r--r--contrib7/omega/OmegaLemmas.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib7/omega/OmegaLemmas.v b/contrib7/omega/OmegaLemmas.v
index b27afd0dd8..a75577e314 100644
--- a/contrib7/omega/OmegaLemmas.v
+++ b/contrib7/omega/OmegaLemmas.v
@@ -10,7 +10,7 @@
Require ZArith_base.
-Open Scope Z_scope.
+Open Local Scope Z_scope.
(** These are specific variants of theorems dedicated for the Omega tactic *)