Compatibility with coq/coq#16756 (#1541)

mit-plv · Dec 11, 2022 · 671cf28 · 671cf28
1 parent 39e1afa
commit 671cf28
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v b/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
@@ -340,7 +340,7 @@ Section with_parameters.
     : map f (upd l i a) = upd (map f l) i (f a).
   Proof.
     eapply nth_error_ext;
-      intros.
+      intros i0.
     destruct (Nat.compare_spec i0 (length l)); subst.
     1,3: rewrite !ListUtil.nth_error_length_error; eauto;
     repeat rewrite ?List.map_length, ?List.upd_length; lia.