From 8218d3f004726e4758612a4fa0951e89ac4c9a74 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 7 Nov 2023 13:10:14 -0800 Subject: [PATCH] fix: Do not show parent state in continue --- Pantograph.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph.lean b/Pantograph.lean index 2532d75..f9f8cc6 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -200,7 +200,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goalStates := state.goalStates.insert nextStateId nextGoalState, nextId := state.nextId + 1 } - let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options) + let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) return .ok { nextStateId? := .some nextStateId, goals? := .some goals,