From b4a7ba86bbd7e4cfcbd2dd24488aa469a95e34cb Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 10 Jan 2018 16:12:20 -0800
Subject: [PATCH] Better follow naming convention: biIndex.

---
 theories/bi/monpred.v              | 16 ++++++++--------
 theories/proofmode/monpred.v       | 10 +++++-----
 theories/tests/proofmode_monpred.v |  2 +-
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 6821c6aa0..5a93ba49e 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 def939542..10948e7ce 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 a18ce8ef0..7ed60b324 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).
-- 
GitLab