From d8ea89528a22f7a3ef2cecdf36a0e671c185973d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Aug 2022 14:35:58 +0200
Subject: [PATCH] Make BI classes consistent: always use `PROP:Type` instead of
 `bi`.

---
 iris/bi/internal_eq.v | 2 +-
 iris/bi/plainly.v     | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 6dd1a42a7..0cf55bb45 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -6,7 +6,7 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
 can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
 [▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
-Class InternalEq (PROP : bi) :=
+Class InternalEq (PROP : Type) :=
   internal_eq : ∀ {A : ofe}, A → A → PROP.
 Global Arguments internal_eq {_ _ _} _ _ : simpl never.
 Global Hint Mode InternalEq ! : typeclass_instances.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 81c8c326b..4109333d9 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -6,15 +6,15 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
 (* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
-Class Plainly (A : Type) := plainly : A → A.
-Global Arguments plainly {A}%type_scope {_} _%I.
+Class Plainly (PROP : Type) := plainly : PROP → PROP.
+Global Arguments plainly {PROP}%type_scope {_} _%I.
 Global Hint Mode Plainly ! : typeclass_instances.
 Global Instance: Params (@plainly) 2 := {}.
 Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
-  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
+  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (PROP:=PROP));
 
   bi_plainly_mixin_plainly_mono (P Q : PROP) : (P ⊢ Q) → ■ P ⊢ ■ Q;
   bi_plainly_mixin_plainly_elim_persistently (P : PROP) : ■ P ⊢ <pers> P;
-- 
GitLab