diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-06 11:59:06 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-06 11:59:06 -0400 |
| commit | 6d27149299a6aaaca3d82480c1b0e90a98cc18a7 (patch) | |
| tree | dc587b6a65b937c11e4bcdb2c9c8df3a26b630f8 /src/ModularArithmetic/ModularBaseSystemListProofs.v | |
| parent | f2c6c26737e97e539d09945cd0b429971bc8b09b (diff) | |
Moved conversion logic out of Pow2BaseProofs into its own file
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemListProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 11b28769b..93b39e89a 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -4,6 +4,7 @@ Require Import Coq.Lists.List. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. Require Import Crypto.BaseSystemProofs. +Require Import Crypto.ModularArithmetic.Conversion. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. @@ -133,7 +134,7 @@ Section LengthProofs. length (pack target_widths_nonneg pf us) = length target_widths. Proof. cbv [pack]; intros. - apply Pow2BaseProofs.length_convert. + apply length_convert. Qed. Lemma length_unpack : forall {target_widths} @@ -142,7 +143,7 @@ Section LengthProofs. length (unpack target_widths_nonneg pf us) = length limb_widths. Proof. cbv [pack]; intros. - apply Pow2BaseProofs.length_convert. + apply length_convert. Qed. End LengthProofs. |