From 61cf8bf1795124a5f103c13954044c71b0532865 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Aug 2020 15:38:44 +0200
Subject: [PATCH] =?UTF-8?q?Fix=20for=20Coq=20=E2=89=A48.9.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/list.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 8cf8eb91..0615e875 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1230,8 +1230,7 @@ Lemma insert_replicate_lt x y n i :
   i < n →
   <[i:=y]>(replicate n x) = replicate i x ++ y :: replicate (n - S i) x.
 Proof.
-  revert i. induction n as [|n IH]; [ by lia | ].
-  intros [|i] Hi; simpl.
+  revert i. induction n as [|n IH]; intros [|i] Hi; simpl; [lia..| |].
   - by rewrite Nat.sub_0_r.
   - by rewrite IH by lia.
 Qed.
-- 
GitLab