From 4e0a30d21e882dc7f5edaaa76fb7304972b36275 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Aug 2016 14:58:13 -0700
Subject: [PATCH] chore(frontends/lean/structure_cmd): remove unnecessary
 dependency

---
 src/frontends/lean/structure_cmd.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 83e8363040..43062b5358 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -24,7 +24,6 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/locals.h"
 #include "library/reducible.h"
-#include "library/unifier.h"
 #include "library/module.h"
 #include "library/aliases.h"
 #include "library/annotation.h"