From 5fc07ae09f0af31db8ea7412d132d09d722feae6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 7 Aug 2017 18:31:41 +0200
Subject: [PATCH] Broken exist_mono'

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

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index ca50081f0..d7d8a9a8c 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -138,7 +138,7 @@ Global Instance forall_flip_mono' A :
   Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_forall M A).
 Proof. intros P1 P2; apply forall_mono. Qed.
 Global Instance exist_mono' A :
-  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A).
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_exist M A).
 Proof. intros P1 P2; apply exist_mono. Qed.
 Global Instance exist_flip_mono' A :
   Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A).
-- 
GitLab