From b893801055e58154a1d8f8c45f30688b3fa48d82 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Apr 2018 23:28:57 +0200
Subject: [PATCH] Fix some bad names.

---
 theories/bi/monpred.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 194cfe311..d24572362 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -920,10 +920,10 @@ Proof.
   - intros P. split=> i /=.
     rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
 Qed.
-Global Instance monPred_plainlyC `{BiPlainly PROP} : BiPlainly monPredSI :=
+Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredSI :=
   {| bi_plainly_mixin := monPred_plainly_mixin |}.
 
-Global Instance monPred_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
+Global Instance monPred_bi_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
   BiPlainlyExist PROP â†’ BiPlainlyExist monPredSI.
 Proof.
   split=>?/=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
-- 
GitLab