diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 86966e8c59a41e9f91045e974b428f64d925d31c..9318a52a817927d2536527ab045012cc6ccd9422 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -890,7 +890,7 @@ Proof.
   rewrite HQ. destruct p; simpl; auto using wand_elim_r.
 Qed.
 
-Class IntoIH {PROP : bi} (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
+Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
   into_ih : φ → of_envs Δ ⊢ Q.
 Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
 Proof. by rewrite envs_entails_eq /IntoIH. Qed.