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

chore: remove unnecessary commands

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-09 09:45:07 -08:00
parent 984257af29
commit 923bd321ef
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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