Commit 58fdaa3e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add missing Import.

parent 4d9e16ec
......@@ -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" :=
......
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