diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b8ea167eb375076b688cdaad86f112e9d12dc005..6afa47b6a194b098bbaf6ef278a60ff574cbe1c6 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1493,7 +1493,7 @@ Section option.
   Global Instance cancelable_Some a :
     IdFree a → Cancelable a → Cancelable (Some a).
   Proof.
-    intros Hirr ?? [b|] [c|] ? EQ; inversion_clear EQ.
+    intros Hirr ? n [b|] [c|] ? EQ; inversion_clear EQ.
     - constructor. by apply (cancelableN a).
     - destruct (Hirr b); [|eauto using dist_le with lia].
       by eapply (cmra_validN_op_l 0 a b), (cmra_validN_le n); last lia.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 3fd8fe1689a83ee2bdbc49a5b4fbb055cdb5a92c..9330d77ebb70ac11bbed9ea814fb19ebc3e1d993 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -118,8 +118,8 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
 Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
 Proof.
-  intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
-  induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
+  intros Hij -> x. assert (i = i2 + i1) as -> by lia. revert j x Hij.
+  induction i2 as [|i2 IH]; intros j X Hij; simplify_eq/=;
     [by rewrite coerce_id|by rewrite g_coerce IH].
 Qed.
 Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 2089b469b76cadfe2f7eaa1d4f046780eb25f67f..c418dd97b75798e7000ff57b063bc3212ca12807 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -92,8 +92,8 @@ Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumO :=
 Next Obligation.
   intros ?? n c; rewrite /compl /csum_compl.
   feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-  + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
-  + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
+  + rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
+  + rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
 Qed.
 
 Global Instance csum_ofe_discrete :
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 017254200c3d814df533af8e1f99c6dd12872320..1e6da09a881f15a70382d341f38943f40d07ef94 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -44,7 +44,7 @@ Proof.
 Qed.
 
 Global Instance frac_cancelable (q : frac) : Cancelable q.
-Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+Proof. intros n y z ??. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
 
 Global Instance frac_id_free (q : frac) : IdFree q.
 Proof. intros p _. apply Qp_plus_id_free. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 37b8f8b61ebaf1f686639939d3984f03fcfb7007..ed15a0559722da3c6c6608a769379748a2bd1870 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -436,13 +436,13 @@ Section freshness.
     pred_infinite I →
     ✓ x → (∀ i, m !! i = None → I i → Q (<[i:=x]>m)) → m ~~>: Q.
   Proof.
-    move=> HP ? HQ. eapply alloc_updateP_strong_dep with (f := λ _, x); eauto.
+    move=> HP ? HQ. eapply (alloc_updateP_strong_dep _ _ _ (λ _, x)); eauto.
   Qed.
   Lemma alloc_updateP (Q : gmap K A → Prop) m x :
     ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
   Proof.
     move=>??.
-    eapply alloc_updateP_strong with (I:=λ _, True);
+    eapply (alloc_updateP_strong _ (λ _, True));
     eauto using pred_infinite_True.
   Qed.
   Lemma alloc_updateP_cofinite (Q : gmap K A → Prop) (J : gset K) m x :
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index f6b3a44fc3a076fb4dcf1175d324a6214e7f777f..1988da55ace94d0b8bee4ebed2add8eab70c1bea 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -32,7 +32,7 @@ Proof. apply discrete_cmra_discrete. Qed.
 End ufrac.
 
 Global Instance ufrac_cancelable (q : ufrac) : Cancelable q.
-Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+Proof. intros n y z ??. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
 
 Global Instance ufrac_id_free (q : ufrac) : IdFree q.
 Proof.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b3e6fb96c443918315c65857e8aeaa7bbc75c498..8b443a61b35095e79a23e1f4f81ee662e8a5a329 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -149,7 +149,7 @@ Section cofe.
   Next Obligation.
     intros n c; split=>i x Hin Hv.
     etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
-    repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
+    repeat intro. apply (chain_cauchy c _ i)=>//. by eapply uPred_mono.
   Qed.
 End cofe.
 Arguments uPredO : clear implicits.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index a81009a0d9ea3624793303846878a175cd6b490b..d94391caf2d8f54595dbed41ee44c44a9d028215 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -797,7 +797,7 @@ Qed.
 Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
 Proof. by unseal. Qed.
 Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
-Proof. induction n; first done. rewrite /= monPred_at_later IHn //. Qed.
+Proof. induction n as [|? IHn]; first done. rewrite /= monPred_at_later IHn //. Qed.
 Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index d23eabdd276e433845aad08bc09b5804c86c090e..7d4f4f0b53a600fa18ceb84c43655982e23a9da6 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -716,7 +716,9 @@ Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto.
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
   to_val e1 = None → to_val e2 = None →
   fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
-Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
+Proof.
+  revert Ki1. induction Ki2; intros Ki1; induction Ki1; naive_solver eauto with f_equal.
+Qed.
 
 Lemma alloc_fresh v n σ :
   let l := fresh_locs (dom (gset loc) σ.(heap)) in
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 774fe60df50e62610d1da6700c25106f6b45ad27..ebf94a86747033358269852e0dcf7fed32816f05 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -249,7 +249,7 @@ Section ectx_language.
     prim_step (fill K e1) σ1 κ e2 σ2 efs →
     ∃ e2', e2 = fill K e2' ∧ head_step e1 σ1 κ e2' σ2 efs.
   Proof.
-    intros (κ'&e2''&σ2''&efs''&?HhstepK) [K' e1' e2' HKe1 -> Hstep].
+    intros (κ'&e2''&σ2''&efs''&HhstepK) [K' e1' e2' HKe1 -> Hstep].
     edestruct (step_by_val K) as [K'' ?];
       eauto using val_head_stuck; simplify_eq/=.
     rewrite -fill_comp in HKe1; simplify_eq.
@@ -277,7 +277,7 @@ Section ectx_language.
     - eauto using fill_not_val.
     - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
       by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
-    - intros e1 σ1 κ e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+    - intros e1 σ1 κ e2 σ2 efs Hnval [K'' e1'' e2'' Heq1 -> Hstep].
       destruct (step_by_val K K'' e1 e1'' σ1 κ e2'' σ2 efs) as [K' ->]; eauto.
       rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
       exists (fill K' e2''); rewrite -fill_comp; split; auto.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index fb982fd7cd6ad03be42222bdc14375fc6e1a202c..603391006be668ebc30a8b6e1223414199da8f10 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -310,7 +310,7 @@ Section language.
       t2 = <[i:=e']>t1 ++ efs ∧
       prim_step e σ1 κ e' σ2 efs).
   Proof.
-    intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=.
+    intros [κ [e σ e' σ' efs t11 t12 ?? Hstep]] Hps; simplify_eq/=.
     apply Forall2_app_inv_l in Hps
       as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
     destruct Hps as [e|e1 e2 e3 [_ Hprs]].