From 7676ac9ff44304a63af3f47b979c6c39b381cb7f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 Aug 2020 09:42:50 +0200
Subject: [PATCH] Stop relying on auto-generated names and implicit
 generalization in a few places

---
 theories/list.v    | 2 +-
 theories/numbers.v | 4 ++--
 theories/streams.v | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 669c28aa..b2d2b817 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -600,7 +600,7 @@ Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
 Lemma insert_length l i x : length (<[i:=x]>l) = length l.
 Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
 Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
-Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
+Proof. revert i. induction l as [|?? IHl]. done. intros [|i]. done. apply (IHl i). Qed.
 Lemma list_lookup_total_alter `{!Inhabited A} f l i :
   i < length l → alter f i l !!! i = f (l !!! i).
 Proof.
diff --git a/theories/numbers.v b/theories/numbers.v
index fa5bf53a..932d4a7f 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -787,11 +787,11 @@ Proof.
   intros H <-. revert a b c d H. cut (∀ a b c d : Qp,
     (a < c)%Qc → a + b = c + d →
     ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
-  { intros help a b c d ?.
+  { intros help a b c d Habcd.
     destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
     - auto.
     - destruct (help c d a b); [done..|]. naive_solver.
-    - apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
+    - apply (inj (Qp_plus a)) in Habcd as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
       exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_plus). }
   intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
   destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
diff --git a/theories/streams.v b/theories/streams.v
index cd7c4ebe..b1811214 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -49,6 +49,6 @@ Global Instance shead_proper : Proper ((≡) ==> (=@{A})) shead.
 Proof. by intros ?? [??]. Qed.
 Global Instance stail_proper : Proper ((≡) ==> (≡@{stream A})) stail.
 Proof. by intros ?? [??]. Qed.
-Global Instance slookup_proper : Proper ((≡@{stream A}) ==> (=)) (slookup i).
+Global Instance slookup_proper i : Proper ((≡@{stream A}) ==> (=)) (slookup i).
 Proof. by induction i as [|i IH]; intros s1 s2 Hs; simpl; rewrite Hs. Qed.
 End stream_properties.
-- 
GitLab