From a497bb6ff58c872e5b93cd453096df9033a65d7f Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Mon, 4 Nov 2024 07:56:58 +0100 Subject: [PATCH] Fully qualify Definition for now --- lisa-sets2/src/main/scala/lisa/automation/Substitution.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala index 407a0849..29b81e0e 100644 --- a/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala +++ b/lisa-sets2/src/main/scala/lisa/automation/Substitution.scala @@ -231,7 +231,7 @@ object Substitution: end Apply object Unfold extends ProofTactic: - def apply(using lib: Library, proof: lib.Proof)(definition: Definition)(premise: proof.Fact): proof.ProofTacticJudgement = + def apply(using lib: Library, proof: lib.Proof)(definition: lib.theory.Definition)(premise: proof.Fact): proof.ProofTacticJudgement = ???