From 923bd321ef8009f24859db7de53e3dfcb371cf3d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Jan 2020 09:45:07 -0800
Subject: [PATCH] chore: remove unnecessary commands

---
 src/Init/Lean/Elab/Command.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index d7a0d6112c..86968ee1d3 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -494,8 +494,6 @@ fun stx => do
     e    ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
     type ← Term.inferType stx.val e;
-    e    ← Term.instantiateMVars stx.val e;
-    type ← Term.instantiateMVars stx.val type;
     logInfo stx.val (e ++ " : " ++ type);
     pure ()