Speed up the pipeline by 3x, restoring previous performance

Apparently using `refine eq_refl` rather than `subst <name for evar>;
reflexivity` was resulting in βδ reduction of `chained_carries` in
`carry_mulmod`.  The β reduction resulted in us getting a different
cps'd term.

I do not know why this particular β reduction resulted in a 3x slowdown
in partial reduction; it seems like anything that cared about sharing
should either get sharing from the top-level in `carry_mulmod`, or
should have no difference in sharing between the terms
```coq
(fun n s c p idxs
  => fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs))
 n s c p idxs
```
and
```coq
fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs))
```

This feels fragile, and I am mystified.

Note for the future: I went about debugging this by integrating little
bits of this PR one by one, seeing which one caused the slowdown, and
then, when I realized it was use of `carry_mulmod`, I took the reified
terms and made a goal asserting their equality, and then took the terms
apart with `f_equal` and `extensionality` until I found the difference.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 71be56f24..b143d2e4e 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -309,7 +309,8 @@ Module Positional. Section Positional.
             by (subst; try assumption; auto using Z.div_mod); reflexivity ].
       eapply f_equal2; [|trivial]. eapply f_equal.
       expand_lists ().
-      refine eq_refl.
+      subst carry_mulmod.
+      reflexivity.
     Qed.
   End carry_mulmod.
 End Positional. End Positional.