From 7b1face0f9c7a19ee4b2fe5db4cae3993661793b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Feb 2018 11:49:12 +0100
Subject: [PATCH] Remove type argument that was already in the section.

---
 theories/proofmode/coq_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 86966e8c5..9318a52a8 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.
-- 
GitLab