diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 6821c6aa0447a636fa79de9970afd5f8225fdeeb..5a93ba49e2acc1c030fbfc7935f61c29044c13bf 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -2,7 +2,7 @@ From iris.bi Require Import bi.
 
 (** Definitions. *)
 
-Structure bi_index :=
+Structure biIndex :=
   BiIndex
     { bi_index_type :> Type;
       bi_index_inhabited : Inhabited bi_index_type;
@@ -12,7 +12,7 @@ Structure bi_index :=
 Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
 
 Section Ofe_Cofe.
-Context {I : bi_index} {PROP : bi}.
+Context {I : biIndex} {PROP : bi}.
 Implicit Types i : I.
 
 Record monPred :=
@@ -104,7 +104,7 @@ Arguments monPredC _ _ : clear implicits.
 (** BI and SBI structures. *)
 
 Section Bi.
-Context {I : bi_index} {PROP : bi}.
+Context {I : biIndex} {PROP : bi}.
 Implicit Types i : I.
 Notation monPred := (monPred I PROP).
 Implicit Types P Q : monPred.
@@ -203,7 +203,7 @@ End Bi.
 
 Typeclasses Opaque monPred_pure monPred_emp monPred_plainly.
 
-Program Definition monPred_later_def {I : bi_index} {PROP : sbi}
+Program Definition monPred_later_def {I : biIndex} {PROP : sbi}
         (P : monPred I PROP) : monPred I PROP := MonPred (λ i, ▷ (P i))%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_later_aux {I PROP} : seal (@monPred_later_def I PROP). by eexists. Qed.
@@ -231,7 +231,7 @@ End MonPred.
 Import MonPred.
 
 Section canonical_bi.
-Context (I : bi_index) (PROP : bi).
+Context (I : biIndex) (PROP : bi).
 
 Lemma monPred_bi_mixin : BiMixin (@monPred_ofe_mixin I PROP)
   monPred_entails monPred_emp monPred_pure monPred_and monPred_or
@@ -322,7 +322,7 @@ Canonical Structure monPredI : bi :=
 End canonical_bi.
 
 Section canonical_sbi.
-Context (I : bi_index) (PROP : sbi).
+Context (I : biIndex) (PROP : sbi).
 
 Lemma monPred_sbi_mixin :
   SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure monPred_or
@@ -362,7 +362,7 @@ End canonical_sbi.
 (** Primitive facts that cannot be deduced from the BI structure. *)
 
 Section bi_facts.
-Context {I : bi_index} {PROP : bi}.
+Context {I : biIndex} {PROP : bi}.
 Implicit Types i : I.
 Implicit Types P Q : monPred I PROP.
 
@@ -483,7 +483,7 @@ Qed.
 End bi_facts.
 
 Section sbi_facts.
-Context {I : bi_index} {PROP : sbi}.
+Context {I : biIndex} {PROP : sbi}.
 Implicit Types i : I.
 Implicit Types P Q : monPred I PROP.
 
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index def9395424ab08e3bee0d9308fbc41264a44fd66..10948e7ce6b81e43a4af41dc64d282ac550d90e9 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -2,21 +2,21 @@ From iris.bi Require Export monpred.
 From iris.proofmode Require Import tactics.
 Import MonPred.
 
-Class MakeMonPredAt {I : bi_index} {PROP : bi} (i : I)
+Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
   make_monPred_at : P i ⊣⊢ 𝓟.
 Arguments MakeMonPredAt {_ _} _ _%I _%I.
 Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
 
-Class IsBiIndexRel {I : bi_index} (i j : I) := is_bi_index_rel : i ⊑ j.
+Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i ⊑ j.
 Hint Mode IsBiIndexRel + - - : typeclass_instances.
-Instance is_bi_index_rel_refl {I : bi_index} (i : I) : IsBiIndexRel i i | 0.
+Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
 Proof. by rewrite /IsBiIndexRel. Qed.
 Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
             : typeclass_instances.
 
 Section bi.
-Context {I : bi_index} {PROP : bi}.
+Context {I : biIndex} {PROP : bi}.
 Local Notation monPred := (monPred I PROP).
 Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
 Implicit Types P Q R : monPred.
@@ -324,7 +324,7 @@ Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
      : typeclass_instances.
 
 Section sbi.
-Context {I : bi_index} {PROP : sbi}.
+Context {I : biIndex} {PROP : sbi}.
 Local Notation monPred := (monPred I PROP).
 Implicit Types P Q R : monPred.
 Implicit Types 𝓟 𝓠 𝓡 : PROP.
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index a18ce8ef0eeeb5d60a23538a274dd37c4b9a921f..7ed60b32487cda2e173087a31a1af5235e9bce40 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic lib.invariants.
 
 Section tests.
-  Context {I : bi_index} {PROP : sbi}.
+  Context {I : biIndex} {PROP : sbi}.
   Local Notation monPred := (monPred I PROP).
   Local Notation monPredI := (monPredI I PROP).
   Local Notation monPredSI := (monPredSI I PROP).