Fix external variables in tracer

JetBrains · Jun 18, 2024 · d5fbaaf · d5fbaaf
1 parent 58a4c17
commit d5fbaaf
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/main/kotlin/org/arend/tracer/ArendTraceAction.kt b/src/main/kotlin/org/arend/tracer/ArendTraceAction.kt
@@ -32,6 +32,7 @@ import org.arend.typechecking.error.local.GoalDataHolder
 import org.arend.typechecking.instance.pool.GlobalInstancePool
 import org.arend.typechecking.visitor.DefinitionTypechecker
 import org.arend.typechecking.visitor.DesugarVisitor
+import org.arend.typechecking.visitor.WhereVarsFixVisitor
 import org.arend.util.ArendBundle
 
 class ArendTraceAction : ArendPopupAction() {
@@ -152,6 +153,7 @@ class ArendTraceAction : ArendPopupAction() {
             var firstTraceEntryIndex = -1
             ActionUtil.underModalProgress(project, ArendBundle.message("arend.tracer.collecting.tracing.data")) {
                 DesugarVisitor.desugar(definition, tracer.errorReporter)
+                WhereVarsFixVisitor.fixDefinition(listOf(definition), tracer.errorReporter)
                 definition.accept(DefinitionTypechecker(tracer, definition.recursiveDefinitions).apply { updateState(false) }, null)
                 firstTraceEntryIndex = tracer.trace.indexOfEntry(expression)
             }