adapt to coq/coq#18563 (#1812)

mit-plv · Jan 30, 2024 · 5d1fa53 · 5d1fa53
1 parent 47058dc
commit 5d1fa53
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.