re-fix syntax so it works on older Coq versions

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.