diff options
Diffstat (limited to 'src/Experiments/NewPipeline/Arithmetic.v')
-rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 6d6dc0f9f..dbb49f0b7 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -2699,15 +2699,14 @@ Module BaseConversion. transitivity (from_associational_inlined sw dw idxs n (rev p)); [ | transitivity (from_associational sw dw idxs n p); [ | reflexivity ] ](* reverse to make addc chains line up *) end. - 2: { - rewrite from_associational_inlined_correct by (subst nout; auto). + { subst widemul_inlined_reverse; reflexivity. } + { rewrite from_associational_inlined_correct by (subst nout; auto). cbv [from_associational]. rewrite !Rows.flatten_partitions' by eauto using Rows.length_from_associational. rewrite !Rows.eval_from_associational by (subst nout; auto). f_equal. rewrite !eval_carries, !Associational.bind_snd_correct, !Associational.eval_rev by auto. reflexivity. } - subst widemul_inlined_reverse; reflexivity. Qed. End widemul. End BaseConversion. |