From adf9f325bf543a9be88103f583b4e0893f512194 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2020 15:38:33 -0800 Subject: [PATCH] fix: holes that should be filled by tatics must be marked as `syntheticOpaque` --- src/Init/Lean/Elab/Tactic.lean | 2 +- src/Init/Lean/Elab/Term.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean index 2ae2bef354..61056dbd27 100644 --- a/src/Init/Lean/Elab/Tactic.lean +++ b/src/Init/Lean/Elab/Tactic.lean @@ -13,7 +13,7 @@ namespace Elab namespace Term def mkTacticMVar (ref : Syntax) (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do -mvar ← mkFreshExprMVar ref type MetavarKind.synthetic `main; +mvar ← mkFreshExprMVar ref type MetavarKind.syntheticOpaque `main; let mvarId := mvar.mvarId!; registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode; pure mvar diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 62ad418433..8a6a3d483b 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -641,7 +641,7 @@ fun stx expectedType? => mkFreshExprMVar stx expectedType? @[builtinTermElab «namedHole»] def elabNamedHole : TermElab := fun stx expectedType? => let name := stx.getIdAt 1; - mkFreshExprMVar stx expectedType? MetavarKind.synthetic name + mkFreshExprMVar stx expectedType? MetavarKind.syntheticOpaque name /-- Main loop for `mkPairs`. -/ private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermElabM Syntax