From 76f697e16de455157615acb3942b8d4b79756262 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 22 Dec 2016 18:43:39 +0100
Subject: [PATCH] remove unused imports

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

diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ad3e7571..54eae3a5 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing type_context lft_contexts perm product own uniq_bor shr_bor.
+From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
 
 Section product_split.
   Context `{typeG Î£}.
-- 
GitLab