chore(tests/lean/run/destruct): fix test

2017-01-21 10:28:46 +01:00 · 2017-01-21 10:28:46 +01:00 · d4879b74cd
commit d4879b74cd
parent 03e09db70e
1 changed files with 1 additions and 1 deletions
--- a/tests/lean/run/destruct.lean
+++ b/tests/lean/run/destruct.lean
@ -26,5 +26,5 @@ begin
  intro n,
  destruct n,
   dsimp, intros, note h := lt_irrefl 0, cc,
-   dsimp, intros, subst n, reflexivity
+   dsimp, intros, subst n
 end