From 4da40f5d0e974d52fa1120d5565de484c7ee80e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 Sep 2018 10:58:32 -0700
Subject: [PATCH] chore(kernel/quot): remove unnecessary include

---
 src/kernel/quot.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp
index ef080472a4..03b0aa2777 100644
--- a/src/kernel/quot.cpp
+++ b/src/kernel/quot.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 Quotient types.
 */
 #include "util/name_generator.h"
-#include "kernel/old_type_checker.h"
 #include "kernel/quot.h"
 #include "kernel/local_ctx.h"
 #include "kernel/inductive/inductive.h"