max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: holes that should be filled by tatics must be marked as syntheticOpaque

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 15:38:33 -08:00
parent 51904224db
commit adf9f325bf
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Tactic.lean
View file

@ -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

2
src/Init/Lean/Elab/Term.lean
View file

@ -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