From bb2df569bcc4caeee991a54ea696c026b0518a51 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Apr 2022 14:56:22 -0700 Subject: [PATCH] fix: bug at `declare_config_elab` --- src/Lean/Elab/Tactic/Config.lean | 6 ++++-- tests/lean/run/declareConfigElabIssue.lean | 2 ++ 2 files changed, 6 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/declareConfigElabIssue.lean diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean index af97c69b78..3c949b5f3e 100644 --- a/src/Lean/Elab/Tactic/Config.lean +++ b/src/Lean/Elab/Tactic/Config.lean @@ -16,9 +16,11 @@ macro "declare_config_elab" elabName:ident type:ident : command => if optConfig.isNone then return { : $type } else - withoutModifyingState <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do + let c ← withoutModifyingState <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type) - eval (← instantiateMVars c) + Term.synthesizeSyntheticMVarsNoPostponing + instantiateMVars c + eval c ) end Lean.Elab.Tactic diff --git a/tests/lean/run/declareConfigElabIssue.lean b/tests/lean/run/declareConfigElabIssue.lean new file mode 100644 index 0000000000..bdc2fc5509 --- /dev/null +++ b/tests/lean/run/declareConfigElabIssue.lean @@ -0,0 +1,2 @@ +example : True := by + simp (config := (fun (c : Lean.Meta.Simp.Config) => { c with arith := true }) {})