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,