From 4d20fc8b5a9252cf3a3429c0738e4b47da624aaa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2020 19:01:12 -0800 Subject: [PATCH] fix: `preserveOrder` logic --- src/Init/Lean/MetavarContext.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean index daf0495031..d8efa51bbf 100644 --- a/src/Init/Lean/MetavarContext.lean +++ b/src/Init/Lean/MetavarContext.lean @@ -710,11 +710,11 @@ else do throw (Exception.revertFailure mctx lctx toRevert prevDecl) }; let newToRevert := if preserveOrder then toRevert else Array.mkEmpty toRevert.size; - let firstDeclToVisit := if preserveOrder then lctx.getFVar! toRevert.back else getLocalDeclWithSmallestIdx lctx toRevert; - let skipFirst := preserveOrder; + let firstDeclToVisit := getLocalDeclWithSmallestIdx lctx toRevert; + let initSize := newToRevert.size; lctx.foldlFromM (fun (newToRevert : Array Expr) decl => - if skipFirst && decl.index == firstDeclToVisit.index then pure newToRevert + if initSize.any $ fun i => decl.fvarId == (newToRevert.get! i).fvarId! then pure newToRevert else if toRevert.any (fun x => decl.fvarId == x.fvarId!) then pure (newToRevert.push decl.toExpr) else if findLocalDeclDependsOn mctx decl (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) then