From 4ea8db27226ded0ba1bb6cbb795f1aac89a9200a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Sep 2020 13:50:05 -0700 Subject: [PATCH] chore: cleanup --- src/Lean/Meta/Tactic/Target.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/Tactic/Target.lean b/src/Lean/Meta/Tactic/Target.lean index 3b63718a41..c3db6539cf 100644 --- a/src/Lean/Meta/Tactic/Target.lean +++ b/src/Lean/Meta/Tactic/Target.lean @@ -14,8 +14,8 @@ namespace Meta /-- Convert the given goal `Ctx |- target` into `Ctx |- targetNew` using an equality proof `eqProof : target = targetNew`. It assumes `eqProof` has type `target = targetNew` -/ -def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId := do -withMVarContext mvarId $ do +def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId := +withMVarContext mvarId do checkNotAssigned mvarId `replaceTarget; tag ← getMVarTag mvarId; newMVar ← mkFreshExprSyntheticOpaqueMVar targetNew tag; @@ -35,7 +35,7 @@ withMVarContext mvarId $ do ``` to create a checkpoint. -/ def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId := -withMVarContext mvarId $ do +withMVarContext mvarId do checkNotAssigned mvarId `change; target ← getMVarType mvarId; if target == targetNew then pure mvarId @@ -47,7 +47,7 @@ withMVarContext mvarId $ do pure newMVar.mvarId! def change (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId := -withMVarContext mvarId $ do +withMVarContext mvarId do target ← getMVarType mvarId; unlessM (isDefEq target targetNew) $ throwTacticEx `change mvarId