diff options
Diffstat (limited to 'theories/ZArith/Zpow_facts.v')
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index fd8da834d..b862d663b 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -14,7 +14,7 @@ Require Import Zcomplements. Require Export Zpower. Require Import Zdiv. Require Import Znumtheory. -Open Scope Z_scope. +Open Local Scope Z_scope. Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x. Proof. |