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 #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 {