Skip to content
GitLab
Commit 4946e270 authored by Ralf Jung's avatar Ralf Jung
Browse files

remove an unused import

parent 5d1bdb74
Hide whitespace changes
Inline Side-by-side
theories/bi/derived_laws_sbi.v
View file @ 4946e270
From iris.bi Require Export derived_laws_bi.
From iris.algebra Require Import monoid.
From stdpp Require Import hlist.
Module bi.
Import interface.bi.
......
Supports Markdown
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