diff options
author | Jason Gross <jagro@google.com> | 2016-09-08 11:22:45 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-09-08 11:22:45 -0700 |
commit | 3eab786d92b348c1dec33640eec3a02a5a86606b (patch) | |
tree | 91adbd9562c3a952b1714245cc4e64dcccda2f16 /src/ModularArithmetic/ModularBaseSystemListProofs.v | |
parent | 054752ccf0b80bc413e70202a823fd034db6ea6b (diff) |
Fully qualify [Require]s
This way they won't become ambiguous if we add new files
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemListProofs.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 16 |
1 files changed, 8 insertions, 8 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. |