From 58fdaa3e0b22db18314709b826c1f97cf56bcc0f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Jun 2018 21:27:27 +0200
Subject: [PATCH] Add missing Import.

---
 theories/bi/big_op.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 0ad6b7c5a..71f2f7068 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -2,7 +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.
+Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
 (* Notations *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
-- 
GitLab