From 6567b89451109382d885b95ba1625c67d8f2c2fb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 01:39:44 +0100
Subject: [PATCH] Fix small naming inconsistency.

---
 theories/bi/embedding.v | 2 +-
 theories/bi/monpred.v   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 4b7d4b234..635d39dc3 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -42,7 +42,7 @@ Section bi_embedding.
 
   Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
   Proof. apply (ne_proper _). Qed.
-  Global Instance bi_embed_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
+  Global Instance bi_embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
   Proof. solve_proper. Qed.
   Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
   Proof.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0ce6daec6..511c267bf 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -416,7 +416,7 @@ Implicit Types P Q : monPred.
 Global Instance monPred_at_mono :
   Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
 Proof. by move=> ?? [?] ?? ->. Qed.
-Global Instance monPred_at_mono_flip :
+Global Instance monPred_at_flip_mono :
   Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) monPred_at.
 Proof. solve_proper. Qed.
 
@@ -426,7 +426,7 @@ Global Instance monPred_in_proper (R : relation I) :
 Proof. unseal. split. solve_proper. Qed.
 Global Instance monPred_in_mono : Proper (flip (⊑) ==> (⊢)) (@monPred_in I PROP).
 Proof. unseal. split. solve_proper. Qed.
-Global Instance monPred_in_mono_flip : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
+Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
 Proof. solve_proper. Qed.
 
 Global Instance monPred_positive : BiPositive PROP → BiPositive monPredI.
-- 
GitLab