From d4879b74cdb025d857e5628dfabd5dd6b3fa201a Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 21 Jan 2017 10:28:46 +0100
Subject: [PATCH] chore(tests/lean/run/destruct): fix test

---
 tests/lean/run/destruct.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/destruct.lean b/tests/lean/run/destruct.lean
index 23eef38b99..5f8a4c8146 100644
--- 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