From b4149da4a5df358aef6ba32f1d66b0fa813aea66 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 3 Oct 2016 21:59:20 -0400 Subject: fix 8.4 build --- src/Spec/PointEncoding.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Spec') 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. -- cgit v1.2.3