From 5d1fa53dc2b38d29d6cfd782bef0b4544eb21a58 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 29 Jan 2024 21:12:38 -0500 Subject: [PATCH] adapt to coq/coq#18563 (#1812) --- src/Util/ListUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index eda4534525..cc475db2ef 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2245,7 +2245,7 @@ Proof. destruct lt_dec; [ | rewrite nth_error_length_error; rewrite ?List.rev_length; try reflexivity; lia ]. revert dependent n; induction ls as [|x xs IHxs]; cbn [length List.rev]; try lia; try reflexivity; intros; try solve [ destruct n; reflexivity ]; []. - { rewrite nth_error_app, List.rev_length, Nat.sub_succ. + { rewrite ListUtil.nth_error_app, List.rev_length, Nat.sub_succ. destruct lt_dec. { rewrite IHxs by lia. rewrite <- (Nat.succ_pred_pos (length xs - n)) by lia.