Merge branch 'ralf/bi' into 'gen_proofmode'

BI -> Bi, to match our convention

See merge request FP/iris-coq!103

theories/base_logic/upred.v

@@ -351,7 +351,7 @@ Import uPred_unseal.
 
 Local Arguments uPred_holds {_} !_ _ _ /.
 
-Lemma uPred_bi_mixin (M : ucmraT) : BIMixin (ofe_mixin_of (uPred M))
+Lemma uPred_bi_mixin (M : ucmraT) : BiMixin (ofe_mixin_of (uPred M))
   uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
                 (@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
                 uPred_sep uPred_wand uPred_plainly uPred_persistently.
@@ -511,7 +511,7 @@ Proof.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
 
-Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
   uPred_entails uPred_pure uPred_or uPred_impl
   (@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
   uPred_sep uPred_plainly uPred_persistently uPred_later.

theories/bi/fixpoint.v

@@ -5,7 +5,7 @@ Import bi.
 
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
-Class BIMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
+Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
   bi_mono_pred Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
@@ -21,7 +21,7 @@ Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
   (∃ Φ : A -n> PROP, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
 
 Section least.
-  Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}.
+  Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Global Instance least_fixpoint_ne : NonExpansive (bi_least_fixpoint F).
   Proof. solve_proper. Qed.

theories/bi/interface.v

@@ -42,7 +42,7 @@ Section bi_mixin.
   Local Infix "-∗" := bi_wand.
   Local Notation "▷ P" := (sbi_later P).
 
-  Record BIMixin := {
+  Record BiMixin := {
     bi_mixin_entails_po : PreOrder bi_entails;
     bi_mixin_equiv_spec P Q : equiv P Q ↔ (P ⊢ Q) ∧ (Q ⊢ P);
 
@@ -141,7 +141,7 @@ Section bi_mixin.
       bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.
 
-  Record SBIMixin := {
+  Record SbiMixin := {
     sbi_mixin_later_contractive : Contractive sbi_later;
 
     sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y);
@@ -166,7 +166,7 @@ Section bi_mixin.
   }.
 End bi_mixin.
 
-Structure bi := BI {
+Structure bi := Bi {
   bi_car :> Type;
   bi_dist : Dist bi_car;
   bi_equiv : Equiv bi_car;
@@ -184,7 +184,7 @@ Structure bi := BI {
   bi_plainly : bi_car → bi_car;
   bi_persistently : bi_car → bi_car;
   bi_ofe_mixin : OfeMixin bi_car;
-  bi_bi_mixin : BIMixin bi_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or
+  bi_bi_mixin : BiMixin bi_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or
                         bi_impl bi_forall bi_exist bi_internal_eq
                         bi_sep bi_wand bi_plainly bi_persistently;
 }.
@@ -224,7 +224,7 @@ Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
 Arguments bi_plainly {PROP} _%I : simpl never, rename.
 Arguments bi_persistently {PROP} _%I : simpl never, rename.
 
-Structure sbi := SBI {
+Structure sbi := Sbi {
   sbi_car :> Type;
   sbi_dist : Dist sbi_car;
   sbi_equiv : Equiv sbi_car;
@@ -243,10 +243,10 @@ Structure sbi := SBI {
   sbi_persistently : sbi_car → sbi_car;
   sbi_later : sbi_car → sbi_car;
   sbi_ofe_mixin : OfeMixin sbi_car;
-  sbi_bi_mixin : BIMixin sbi_ofe_mixin sbi_entails sbi_emp sbi_pure sbi_and
+  sbi_bi_mixin : BiMixin sbi_ofe_mixin sbi_entails sbi_emp sbi_pure sbi_and
                          sbi_or sbi_impl sbi_forall sbi_exist sbi_internal_eq
                          sbi_sep sbi_wand sbi_plainly sbi_persistently;
-  sbi_sbi_mixin : SBIMixin sbi_entails sbi_pure sbi_or sbi_impl
+  sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
                            sbi_forall sbi_exist sbi_internal_eq
                            sbi_sep sbi_plainly sbi_persistently sbi_later;
 }.