diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index f0fa7ffb1934914d064f3667e761df121d431a95..6940ba8e581f08ef73bedb5260df9e1bf227a769 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -222,7 +222,7 @@ Proof.
   rewrite !multiplicity_disj_union. lia.
 Qed.
 Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
-Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
+Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj (X ⊎.)). Qed.
 
 Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
 Proof.
diff --git a/theories/list.v b/theories/list.v
index 1203a5db8a9052755862aa9ff5f4e8e283787e9e..825b2f096781100bece52fbdcccec567b5740d65 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2232,7 +2232,7 @@ Qed.
 Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
 Proof.
   induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l.
-  intros (?&E%(inj _)&?). apply IH. by rewrite E.
+  intros (?&E%(inj (cons y))&?). apply IH. by rewrite E.
 Qed.
 Lemma submseteq_app_inv_r l1 l2 k : l1 ++ k ⊆+ l2 ++ k → l1 ⊆+ l2.
 Proof.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 2d5038c00c7cf9e0d2a8614b9fdc1c2c29c9d78b..9bd02fcd809864c74bb1f44d026af45e4d0a4bd1 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -58,7 +58,7 @@ Section namespace.
     intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
     unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
     intros [qx ->] [qy Hqy].
-    revert Hqy. by intros [= ?%(inj _)]%positives_flatten_suffix_eq.
+    revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq.
   Qed.
 
   Lemma ndot_preserve_disjoint_l N E x : ↑N ## E → ↑N.@x ## E.
diff --git a/theories/numbers.v b/theories/numbers.v
index 8f2914358c461010faf97feafd6269fdc4c9c3a1..6f03dd236605a1b260d920590d220d85413b8d68 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -710,7 +710,7 @@ Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
 Instance Qp_plus_comm : Comm (=) Qp_plus.
 Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
 Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed.
+Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed.
 Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
 Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
 
@@ -794,9 +794,9 @@ Proof.
     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 _) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
+    - apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
       eauto 10 using (comm_L Qp_plus). }
-  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj _).
+  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'&->&->).
   eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
   - by rewrite (assoc_L _), (comm_L Qp_plus e).
diff --git a/theories/option.v b/theories/option.v
index f658505e880018ead0a31fe45f06996ea5a8d751..f8c284a9159a7554a62ad95d0b4cd400342fceb5 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -189,8 +189,8 @@ Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) m
   f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
 Proof.
   destruct mx; simpl; split.
-  - intros ?%(inj _). eauto.
-  - intros (? & ->%(inj _) & ?). constructor. done.
+  - intros ?%(inj Some). eauto.
+  - intros (? & ->%(inj Some) & ?). constructor. done.
   - intros ?%symmetry%equiv_None. done.
   - intros (? & ? & ?). done.
 Qed.