From df1feae2c1267d998b8cfe789f09d885a93fb1fd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 May 2018 15:02:51 +0200
Subject: [PATCH] remove bi.big_... compatibility aliases for big-ops

---
 tests/proofmode.v                 | 2 +-
 theories/bi/bi.v                  | 8 --------
 theories/bi/big_op.v              | 4 +---
 theories/proofmode/ltac_tactics.v | 8 ++++----
 4 files changed, 6 insertions(+), 16 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 56d90ffdb..4443bbb9d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -185,7 +185,7 @@ Lemma test_TC_resolution `{!BiAffine PROP} (Φ : nat → PROP) l x :
   x ∈ l → ([∗ list] y ∈ l, Φ y) -∗ Φ x.
 Proof.
   iIntros (Hp) "HT".
-  iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
+  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
   done.
 Qed.
 
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 86a7c24b8..95fbe03a9 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -6,16 +6,8 @@ Module Import bi.
   Export bi.interface.bi.
   Export bi.derived_laws_bi.bi.
   Export bi.derived_laws_sbi.bi.
-  (* For better compatibility with some developments created during
-     gen_proofmode times, also provide bigops inside the bi
-     module. *)
-  Export bi.big_op.bi.
 End bi.
 
-(* For better compatibility with pre-gen_proofmode-Iris, also provide
-   bigops outside of the bi module. *)
-Export bi.big_op.bi.
-
 (* Hint DB for the logic *)
 Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : BI.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 477105c84..277d29308 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -2,6 +2,7 @@ From iris.algebra Require Export big_op.
 From iris.bi Require Import derived_laws_sbi plainly.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
+Import interface.bi derived_laws_bi.bi.
 
 (* Notations *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l)
@@ -40,8 +41,6 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
    format "[∗  mset]  x  ∈  X ,  P") : bi_scope.
 
 (** * Properties *)
-Module bi.
-Import interface.bi derived_laws_bi.bi.
 Section bi_big_op.
 Context {PROP : bi}.
 Implicit Types Ps Qs : list PROP.
@@ -876,4 +875,3 @@ Section gmultiset.
   End plainly.
 End gmultiset.
 End sbi_big_op.
-End bi.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index db8bce58e..3874e71e4 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2096,13 +2096,13 @@ below; see the discussion in !75 for further details. *)
 Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
   rewrite envs_entails_eq; apply bi.internal_eq_refl.
 Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepL_nil'.
+  rewrite envs_entails_eq; apply big_sepL_nil'.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepM_empty'.
+  rewrite envs_entails_eq; apply big_sepM_empty'.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepS_empty'.
+  rewrite envs_entails_eq; apply big_sepS_empty'.
 Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepMS_empty'.
+  rewrite envs_entails_eq; apply big_sepMS_empty'.
 
 Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
 Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.
-- 
GitLab