From 73543f127942ddbe1369bedb2db417fda715b8f6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Oct 2015 19:06:46 -0700
Subject: [PATCH] fix(library/norm_num): use new type-class resolution
 procedure at norm_num

---
 src/library/class_instance_resolution.h | 1 +
 src/library/norm_num.h                  | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/library/class_instance_resolution.h b/src/library/class_instance_resolution.h
index e4cabd778..9691e8a9a 100644
--- a/src/library/class_instance_resolution.h
+++ b/src/library/class_instance_resolution.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include "kernel/environment.h"
+#include "kernel/pos_info_provider.h"
 #include "library/io_state.h"
 #include "library/local_context.h"
 
diff --git a/src/library/norm_num.h b/src/library/norm_num.h
index 68fd66cd8..5a279eb4f 100644
--- a/src/library/norm_num.h
+++ b/src/library/norm_num.h
@@ -7,7 +7,7 @@ Author: Robert Y. Lewis
 #include "kernel/environment.h"
 #include "library/local_context.h"
 #include "library/num.h"
-#include "library/class_instance_synth.h"
+#include "library/class_instance_resolution.h"
 
 namespace lean {
 class norm_num_context {