use goal lctx for hints

Closes #135
leanprover-community · Nov 30, 2023 · 97dc648 · 97dc648
1 parent 472e2c6
commit 97dc648
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean
@@ -126,7 +126,7 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
           then
             let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
             let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
-            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
             return some { text := text, hidden := hint.hidden }
           else return none