Skip to content

Commit 930f7c8

Browse files
Merge PR rocq-prover#18606: Fix bug introduced in rocq-prover#18564 (deprecation of stdlib map_length)
Reviewed-by: herbelin Co-authored-by: herbelin <[email protected]>
2 parents 5905edd + f24b343 commit 930f7c8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

theories/Lists/List.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3577,7 +3577,7 @@ Global Hint Rewrite
35773577
rev_involutive (* rev (rev l) = l *)
35783578
rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
35793579
map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
3580-
length_app (* length (map f l) = length l *)
3580+
length_map (* length (map f l) = length l *)
35813581
length_seq (* length (seq start len) = len *)
35823582
length_app (* length (l ++ l') = length l + length l' *)
35833583
length_rev (* length (rev l) = length l *)

0 commit comments

Comments
 (0)