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

chore: minor

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-29 12:39:13 -08:00
parent e102cd4f42
commit 32f219772c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/MetavarContext.lean
View file

@ -895,7 +895,7 @@ mutual
let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
-- Remark: we must reset the before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
let newMVarId ← get >>= fun s => pure s.ngen.curr
let newMVarId := (← get).ngen.curr
let newMVar := mkMVar newMVarId
let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs