From 0ffb7c080fab8cb858d222009e7de1ad3fc0ed3d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Jan 2015 12:11:52 -0800
Subject: [PATCH] fix(tests/lean/run/inv_bug2): adjust test to reflect changes
 at data.vector

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

diff --git a/tests/lean/run/inv_bug2.lean b/tests/lean/run/inv_bug2.lean
index 501c78be1e..24a891e343 100644
--- a/tests/lean/run/inv_bug2.lean
+++ b/tests/lean/run/inv_bug2.lean
@@ -7,7 +7,7 @@ namespace vector
   protected definition destruct2 (v : vector A (succ (succ n))) {P : Π {n : nat}, vector A (succ n) → Type}
                                  (H : Π {n : nat} (h : A) (t : vector A n), P (h :: t)) : P v :=
   begin
-    cases v with (h', n', t'),
+    cases v with (n', h', t'),
     apply (H h' t')
   end
 end vector