From 6f43ded103e47b4cf81f3c78909c3f1aa0bcf750 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 11 Nov 2016 16:17:22 -0500 Subject: use @implicits in rewrite (8.4) --- src/Util/Tuple.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index af9d9816c..0d8a1582a 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -251,8 +251,8 @@ Qed. Ltac tuple_maps_to_list_maps := try eapply to_list_ext; tuples_from_lists; - repeat (rewrite <-map_to_list || rewrite <-to_list_map2 || - rewrite to_list_from_list || rewrite from_list_to_list). + repeat (rewrite <-@map_to_list || rewrite <-@to_list_map2 || + rewrite @to_list_from_list || rewrite @from_list_to_list). Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n) : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys. -- cgit v1.2.3