From f590d3b5cf418e77cd5c722de1996ae82c849faa Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 11 May 2021 23:47:28 +0200
Subject: [PATCH] Useless import
---
theories/typing/base.v | 1 -
1 file changed, 1 deletion(-)
diff --git a/theories/typing/base.v b/theories/typing/base.v
index f5cb2484..3ccbee1f 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,5 +1,4 @@
From lrust.lang Require Export proofmode.
-From lrust.lifetime Require Export frac_borrow.
(* Last, so that we make sure we shadow the defintion of delete for
sets coming from the prelude. *)
--
GitLab