From ba88a3b05a6c054a857efc0c51d63957542addd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 15:40:56 -0800 Subject: [PATCH] chore(builtin/heq): remove unnecessary import Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 64fed7f58..5bc638247 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -1,5 +1,3 @@ -import macros - -- Heterogenous equality variable heq {A B : TypeU} : A → B → Bool infixl 50 == : heq