diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-13 14:59:57 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-13 14:59:57 -0400 |
| commit | 4209a1f2ea8f41f35c219e354f2796f746481225 (patch) | |
| tree | ddecb61d40752e6dda92426ca9bbe9ac94a1e67d /src/BoundedArithmetic/Double | |
| parent | 0ce75d20f86a287a1b179bd429b30d758f1c4716 (diff) | |
Work around bug 5401 (bad let '(x, y))
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5140, destructuring
let under binders of a class with an argument gives "Anomaly: index to
an anonymous variable. Please report at http://coq.inria.fr/bugs/."
Diffstat (limited to 'src/BoundedArithmetic/Double')
| -rw-r--r-- | src/BoundedArithmetic/Double/Core.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/BoundedArithmetic/Double/Core.v b/src/BoundedArithmetic/Double/Core.v index 011c610ec..94d18673c 100644 --- a/src/BoundedArithmetic/Double/Core.v +++ b/src/BoundedArithmetic/Double/Core.v @@ -31,12 +31,12 @@ Section ripple_carry_definitions. | O => f | S k' => fun xss yss carry => dlet xss := xss in dlet yss := yss in - let '(xs, x) := eta xss in - let '(ys, y) := eta yss in + let (xs, x) := eta xss in + let (ys, y) := eta yss in dlet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in - let '(carry, zs) := eta addv in + let (carry, zs) := eta addv in dlet fxy := (f x y carry) in - let '(carry, z) := eta fxy in + let (carry, z) := eta fxy in (carry, (zs, z)) end. @@ -204,10 +204,10 @@ Section tuple2. dlet out := out in dlet tmp := mulhwhl a b in dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in - let '(_, out) := eta addv in + let (_, out) := eta addv in dlet tmp := mulhwhl b a in dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in - let '(_, out) := eta addv in + let (_, out) := eta addv in out. (** Require a dummy [decoder] for these instances to allow |