Fix bug introduced in coq#18564

proux01 · Feb 1, 2024 · f24b343 · f24b343
1 parent 511511c
commit f24b343
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
@@ -3577,7 +3577,7 @@ Global Hint Rewrite
   rev_involutive (* rev (rev l) = l *)
   rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
   map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
-  length_app (* length (map f l) = length l *)
+  length_map (* length (map f l) = length l *)
   length_seq (* length (seq start len) = len *)
   length_app (* length (l ++ l') = length l + length l' *)
   length_rev (* length (rev l) = length l *)