diff options
| author | Vincent Laporte | 2019-10-10 09:55:30 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-22 06:38:20 +0000 |
| commit | f0014b4c9bbfa840c952b8943934056a7b0a446e (patch) | |
| tree | 8c2d77cb47d5b888c06e32535f078878a41d7230 /theories/ZArith/Zpow_facts.v | |
| parent | c887547a927d43fdcf3d1031d360c0036e7e252d (diff) | |
Znumtheory: do not use “omega”
Diffstat (limited to 'theories/ZArith/Zpow_facts.v')
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 8ba511940e..e65eb7cdc7 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -8,8 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory. -Import Omega. +Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory. Require Export Zpower. Local Open Scope Z_scope. |