From 481cc35d5d886845d4afdf949d9b93313e1b1d92 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anja=20Petkovi=C4=87=20Komel?= Date: Tue, 1 Oct 2024 14:29:32 +0200 Subject: [PATCH] add missing includes --- Inferences/Induction.hpp | 1 + Inferences/SubsumptionDemodulationHelper.hpp | 1 + Kernel/MLMatcher.hpp | 2 ++ Kernel/MLMatcherSD.hpp | 2 ++ Kernel/UnificationWithAbstraction.cpp | 2 ++ 5 files changed, 8 insertions(+) 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"