use goal lctx for hints

Closes #135
1 year ago · 97dc648452
parent 472e2c66df
commit 97dc648452
1 changed files with 1 additions and 1 deletions
--- 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