diff options
author | jadep <jade.philipoom@gmail.com> | 2018-09-15 12:55:22 -0400 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-09-17 21:34:36 -0400 |
commit | 61f6a2d25c657372022395c9fce329e6bc11c409 (patch) | |
tree | 652112288b0626a6c4774d6b6aac368069b02d08 /src/Experiments/NewPipeline/Arithmetic.v | |
parent | 6d22687d2e9f8842f05e7f8788fcf3278e5627fc (diff) |
re-fix syntax so it works on older Coq versions
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. |