From 25e7b53dcdcd96f63149f6a0c54845261b88a1f3 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Fri, 17 Jan 2025 13:33:21 +0100
Subject: [PATCH] ind -> i

---
 stdpp/list.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/stdpp/list.v b/stdpp/list.v
index eb7c0e5c..b1628085 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5056,18 +5056,18 @@ Section zip.
   Lemma zip_nil_inv l k :
     zip l k = [] ↔ l = [] ∨ k = [].
   Proof. by induction l; induction k; naive_solver. Qed.
-  Lemma lookup_zip_split l k ind e1 e2 :
-    zip l k !! ind = Some (e1, e2) ↔ l !! ind = Some e1 ∧ k !! ind = Some e2.
+  Lemma lookup_zip_split l k i e1 e2 :
+    zip l k !! i = Some (e1, e2) ↔ l !! i = Some e1 ∧ k !! i = Some e2.
   Proof.
-    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl;
+    induction l as [| hd1 tail1 IH1] in k,i |-*; destruct k as [ | y ys]; simpl;
       [ naive_solver.. | ].
-    case ind as [| ind']; naive_solver.
+    case i as [| ind']; naive_solver.
   Qed.
-  Lemma lookup_zip_None l k ind :
-    zip l k !! ind = None ↔ l !! ind = None ∨ k !! ind = None.
+  Lemma lookup_zip_None l k i :
+    zip l k !! i = None ↔ l !! i = None ∨ k !! i = None.
   Proof.
-   by induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl;
-      case ind; naive_solver.
+   by induction l as [| hd1 tail1 IH1] in k,i |-*; destruct k as [ | y ys]; simpl;
+      case i; naive_solver.
   Qed.
 End zip.
 
-- 
GitLab