From e96d5cf811fe91b18f9e4487224a52590635c2a1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 2 Dec 2016 12:52:31 +0100
Subject: [PATCH] Flipped Proper for uPred_valid.

---
 base_logic/primitive.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 299d9cd30..ed8841b31 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -322,6 +322,9 @@ Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
 Proof. solve_proper. Qed.
 Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
 Proof. solve_proper. Qed.
+Global Instance uPred_valid_flip_mono :
+  Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
 
 (** Introduction and elimination rules *)
 Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.
-- 
GitLab