diff options
| author |  jadep <jadep@mit.edu> | 2019-03-14 15:04:10 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | a189b8ad9943cec026ea2797789d8dc72a6d3336 (patch) | |
| tree | 727a7957ee921526a701a8a50fb91209b9ee2b56 /src/Arithmetic/BaseConversion.v | |
| parent | 9c5a967ababd80425fe3b09f17f502ed5f0d6a11 (diff) | |
remove extraneous module identifiers
Diffstat (limited to 'src/Arithmetic/BaseConversion.v')
| -rw-r--r-- | src/Arithmetic/BaseConversion.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Arithmetic/BaseConversion.v b/src/Arithmetic/BaseConversion.v index c06dd3d71..dde04ae2a 100644 --- a/src/Arithmetic/BaseConversion.v +++ b/src/Arithmetic/BaseConversion.v @@ -215,14 +215,14 @@ Module BaseConversion. Lemma widemul_correct a b : length a = m -> length b = m -> - widemul a b = Partition.partition sw nout (seval m a * seval m b). + widemul a b = partition sw nout (seval m a * seval m b). Proof. apply mul_converted_partitions; auto with zarith. Qed. Derive widemul_inlined SuchThat (forall a b, length a = m -> length b = m -> - widemul_inlined a b = Partition.partition sw nout (seval m a * seval m b)) + widemul_inlined a b = partition sw nout (seval m a * seval m b)) As widemul_inlined_correct. Proof. intros. @@ -238,7 +238,7 @@ Module BaseConversion. SuchThat (forall a b, length a = m -> length b = m -> - widemul_inlined_reverse a b = Partition.partition sw nout (seval m a * seval m b)) + widemul_inlined_reverse a b = partition sw nout (seval m a * seval m b)) As widemul_inlined_reverse_correct. Proof. intros. |