diff --git a/theories/list.v b/theories/list.v
index 669c28aab083a3b0eee19ccb5f83cc10de1f78e9..b2d2b81771116422885ad62bd5d4713557436da4 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 fa5bf53ab49c8e2d4dfd523c825edfba421a2f72..932d4a7f69a4b98165659563a9fc6ccc6a4ca355 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 cd7c4ebeca0e87a56fa981ed145edd223cd63548..b1811214d0783819c801f1d5079417ca12c91904 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.