diff options
author | 2016-09-08 11:22:45 -0700 | |
---|---|---|
committer | 2016-09-08 11:22:45 -0700 | |
commit | 3eab786d92b348c1dec33640eec3a02a5a86606b (patch) | |
tree | 91adbd9562c3a952b1714245cc4e64dcccda2f16 /src/ModularArithmetic | |
parent | 054752ccf0b80bc413e70202a823fd034db6ea6b (diff) |
Fully qualify [Require]s
This way they won't become ambiguous if we add new files
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 16 | ||||
-rw-r--r-- | src/ModularArithmetic/Pow2Base.v | 2 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 6 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParams.v | 4 |
4 files changed, 14 insertions, 14 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 16699b8a2..48c4f2402 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -1,7 +1,7 @@ -Require Import Zpower ZArith. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import List. -Require Import VerdiTactics. +Require Import Coq.Lists.List. +Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystemProofs. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. @@ -58,8 +58,8 @@ Section LengthProofs. | |- 2 ^ _ <> 0 => apply Z.pow_nonzero | |- _ => solve [apply BaseSystem.b0_1] | |- _ => solve [auto using limb_widths_nonneg, sum_firstn_limb_widths_nonneg, limb_widths_match_modulus] - | |- _ => omega - | |- _ => congruence + | |- _ => omega + | |- _ => congruence end. Qed. @@ -117,7 +117,7 @@ Section LengthProofs. apply Min.min_case; omega. Qed. Hint Rewrite @length_conditional_subtract_modulus : distr_length. - + Lemma length_freeze {u} : length u = length limb_widths -> length (freeze u) = length limb_widths. @@ -133,7 +133,7 @@ Section LengthProofs. cbv [pack]; intros. apply Pow2BaseProofs.length_convert. Qed. - + Lemma length_unpack : forall {target_widths} {target_widths_nonneg : forall x, In x target_widths -> 0 <= x} {pf us}, @@ -143,4 +143,4 @@ Section LengthProofs. apply Pow2BaseProofs.length_convert. Qed. -End LengthProofs.
\ No newline at end of file +End LengthProofs. diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index bb2f34ad4..0175018f8 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -1,4 +1,4 @@ -Require Import Zpower ZArith. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.ZUtil. Require Crypto.BaseSystem. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 4b3af84e1..630fc102e 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -1,9 +1,9 @@ -Require Import Zpower ZArith. -Require Import List. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.BaseSystem. Require Import Crypto.BaseSystemProofs. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index 1f9a0f2f6..b564bcb05 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -1,5 +1,5 @@ -Require Import ZArith. -Require Import List. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil. Require Crypto.BaseSystem. Local Open Scope Z_scope. |