From 1c5ec65260dd50eaa3a57cb74250dfc2bc668b4d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Aug 2022 07:30:29 -0700
Subject: [PATCH] chore: `runTermElabM` refactor

---
 Lake/DSL/Meta.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lake/DSL/Meta.lean b/Lake/DSL/Meta.lean
index 8a122c291c..18eba33904 100644
--- a/Lake/DSL/Meta.lean
+++ b/Lake/DSL/Meta.lean
@@ -53,7 +53,7 @@ scoped syntax (name := metaIf)
 "meta " "if " term " then " cmdDo (" else " cmdDo)? : command
 
 elab_rules : command | `(meta if $c then $t $[else $e?]?) => do
-  if (← withRef c <| runTermElabM none <| fun _ => evalTerm Bool c) then
+  if (← withRef c <| runTermElabM fun _ => evalTerm Bool c) then
     let cmd := mkNullNode (expandCmdDo t)
     withMacroExpansion (← getRef) cmd <| elabCommand cmd
   else if let some e := e? then