From e8181464416170f8b883968007d936559b3c5df1 Mon Sep 17 00:00:00 2001 From: Hoang-Hai Dang <haidang@mpi-sws.org> Date: Fri, 28 Jun 2019 21:54:36 +0200 Subject: [PATCH] remove unneeded import --- theories/typing/type.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/typing/type.v b/theories/typing/type.v index 7672f3cf..0e2ed5ec 100644 --- a/theories/typing/type.v +++ b/theories/typing/type.v @@ -1,6 +1,6 @@ From gpfsl.lang Require Export notation. From gpfsl.base_logic Require Export na. -From gpfsl.logic Require Export na_invariants view_invariants. +From gpfsl.logic Require Export na_invariants. From lrust.lifetime Require Export frac_borrow. From lrust.typing Require Export base. From lrust.typing Require Import lft_contexts. -- GitLab