diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index 9f46ca094..8bf07cfd7 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -19,6 +19,7 @@ #include #include #include +#include #include "Forwards.hpp" diff --git a/Inferences/SubsumptionDemodulationHelper.hpp b/Inferences/SubsumptionDemodulationHelper.hpp index 73b6db287..48adb4a49 100644 --- a/Inferences/SubsumptionDemodulationHelper.hpp +++ b/Inferences/SubsumptionDemodulationHelper.hpp @@ -12,6 +12,7 @@ #define SUBSUMPTIONDEMODULATIONHELPER_HPP #include +#include #include "Indexing/LiteralMiniIndex.hpp" #include "Kernel/Clause.hpp" diff --git a/Kernel/MLMatcher.hpp b/Kernel/MLMatcher.hpp index aa272bbb1..e50c42825 100644 --- a/Kernel/MLMatcher.hpp +++ b/Kernel/MLMatcher.hpp @@ -19,6 +19,8 @@ #include "Forwards.hpp" #include "Clause.hpp" +#include + namespace Kernel { using namespace Lib; diff --git a/Kernel/MLMatcherSD.hpp b/Kernel/MLMatcherSD.hpp index 44857f871..6438347f7 100644 --- a/Kernel/MLMatcherSD.hpp +++ b/Kernel/MLMatcherSD.hpp @@ -14,6 +14,8 @@ #include "Clause.hpp" #include "Forwards.hpp" +#include + namespace Kernel { using namespace Lib; diff --git a/Kernel/UnificationWithAbstraction.cpp b/Kernel/UnificationWithAbstraction.cpp index 4f85491a3..da2e362fd 100644 --- a/Kernel/UnificationWithAbstraction.cpp +++ b/Kernel/UnificationWithAbstraction.cpp @@ -13,6 +13,8 @@ * */ +#include + #include "Lib/Backtrackable.hpp" #include "Lib/Coproduct.hpp" #include "Shell/Options.hpp"