From df6c2f124fce4cecd42da806a003afdf3a922c09 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Fri, 3 Apr 2026 14:21:40 +0800
Subject: feat: implement substitution logic and unify/applySubstitution
 functions for term resolution

---
 proofsearch/CMakeLists.txt | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofsearch/CMakeLists.txt')

diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt
index 2cf69db..edeb6b7 100644
--- a/proofsearch/CMakeLists.txt
+++ b/proofsearch/CMakeLists.txt
@@ -72,6 +72,7 @@ set(ATP_SOURCES
     src/core/term_bank.cc
     src/core/clause_store.cc
     src/normalize/clausifier.cc
+    src/infer/substitution.cc
     src/infer/unification.cc
     src/infer/resolution.cc
     src/index/discrim_tree.cc
-- 
cgit v1.2.3