Fix segfault triggered by codegen bug (#183)

leanprover-community · Dec 5, 2024 · 1c1c651 · 1c1c651
1 parent 8b6048a
commit 1c1c651
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean
@@ -315,6 +315,8 @@ inductive Feature
 
 namespace Feature
 
+-- Workaround for codegen bug, see #182
+set_option compiler.extract_closed false in
 partial def «elab» (stx : Syntax) : ElabM Feature :=
   withRef stx do
     match stx with
@@ -330,7 +332,7 @@ partial def «elab» (stx : Syntax) : ElabM Feature :=
         let nonIdentAlts :=
           stx.getArgs.filter λ stx => ! stx.isOfKind ``Parser.featIdent
         if h : nonIdentAlts.size = 1 then
-          return ← «elab» $ nonIdentAlts[0]'(by simp [h])
+          return ← «elab» $ nonIdentAlts[0]
       throwUnsupportedSyntax
 
 end Feature