diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-11 16:17:22 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-11 19:31:09 -0500 |
| commit | 6f43ded103e47b4cf81f3c78909c3f1aa0bcf750 (patch) | |
| tree | 730356f4fd63a0f41de68a3c3496ff9382b5a929 /src/Util/Tuple.v | |
| parent | 4e418c9f91f7cd35c18e853f7d743b888d01fde1 (diff) | |
use @implicits in rewrite (8.4)
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |