From fdbd962742482ab78bce105315170a4edcad41e4 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 26 Jan 2023 12:17:26 +0100
Subject: [PATCH] set_option tactic.hygienic false

Fixes #28
---
 server/leanserver/GameServer/FileWorker.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index e0470fe..0d369eb 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -104,7 +104,9 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
-          let cmdStx ← `(command| theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+          let cmdStx ← `(command|
+            set_option tactic.hygienic false in
+            theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post