diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index c34324351ae23a06dda4e2cba17d62ceb50844e9..ca132298d9690bb3c92d8206958113a63013fb7c 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -45,7 +45,7 @@ Section bi_embedding.
   Proof. solve_proper. Qed.
   Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
   Proof.
-    intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
+    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
     rewrite EQ //.
   Qed.