From 4946e27027056b6d8d30d1729ee821823cdcac66 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Jun 2018 21:26:30 +0200
Subject: [PATCH] remove an unused import

---
 theories/bi/derived_laws_sbi.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index d1afdc565..842fcdaa1 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -1,6 +1,5 @@
 From iris.bi Require Export derived_laws_bi.
 From iris.algebra Require Import monoid.
-From stdpp Require Import hlist.
 
 Module bi.
 Import interface.bi.
-- 
GitLab