Commit df1feae2 authored by Ralf Jung's avatar Ralf Jung

remove bi.big_... compatibility aliases for big-ops

parent 54efc60b
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment