From 2e76d24c2960ed14dc19dcc5b02fc85c93e082b3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Oct 2018 21:42:00 +0200
Subject: [PATCH] Close issue #218.

---
 theories/proofmode/class_instances_bi.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index d1adf1666..1bf5121e8 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -10,11 +10,11 @@ Implicit Types P Q R : PROP.
 Implicit Types mP : option PROP.
 
 (** AsEmpValid *)
-Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
+Global Instance as_emp_valid_emp_valid (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
 Proof. by rewrite /AsEmpValid. Qed.
-Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
+Global Instance as_emp_valid_entails (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
 Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
-Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
+Global Instance as_emp_valid_equiv (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
 Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 
 Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
-- 
GitLab