diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-03 21:59:20 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-03 21:59:20 -0400 |
| commit | b4149da4a5df358aef6ba32f1d66b0fa813aea66 (patch) | |
| tree | dd8f40f98ef6a464b8e8d67719fe38dd950eb4ff /src/Spec | |
| parent | 1283ca66b0280250071696377a4ca19bc809beea (diff) | |
fix 8.4 build
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/PointEncoding.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 6c6e3fa9d..99726f311 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -361,7 +361,7 @@ Section PointEncoding. rewrite option_map_option_rect. eapply option_rect_shuffle with (EQD := Keq). + apply Algebra.monoid_Equivalence. - + apply Tuple.Equivalence_fieldwise. + + apply (@Tuple.Equivalence_fieldwise K _ _ 2). + apply Proper_Kcoordinates_from_y; auto. + cbv [Encoding.dec Fencoding]. apply phi_decode. |