From 81b17d8c9f40c4d6a00be3b56fbd16560d9a8a6f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 10:59:36 +0100
Subject: [PATCH] Remove unused premise of iso_cofe_subtype.

---
 theories/algebra/ofe.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index def249e5a..a6721f962 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1147,7 +1147,6 @@ Qed.
 
 Section iso_cofe_subtype.
   Context {A B : ofeT} `{Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
-  Context (Pg : ∀ y, P (g y)).
   Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
   Let Hgne : NonExpansive g.
   Proof. intros n y1 y2. apply g_dist. Qed.
-- 
GitLab