From 3eab786d92b348c1dec33640eec3a02a5a86606b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Sep 2016 11:22:45 -0700 Subject: Fully qualify [Require]s This way they won't become ambiguous if we add new files --- src/ModularArithmetic/ModularBaseSystemListProofs.v | 16 ++++++++-------- src/ModularArithmetic/Pow2Base.v | 2 +- src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 6 +++--- src/ModularArithmetic/PseudoMersenneBaseParams.v | 4 ++-- 4 files changed, 14 insertions(+), 14 deletions(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3