From efc33a2f1db2f7cff42f0e4f73d3f325846218dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 May 2015 13:01:37 -0700
Subject: [PATCH] fix(tests/lean): adjusts tests

---
 tests/lean/hott/cases_eq.hlean |  2 +-
 tests/lean/hott/inj_tac.hlean  | 14 +++++++++++---
 tests/lean/run/tactic17.lean   |  2 +-
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/tests/lean/hott/cases_eq.hlean b/tests/lean/hott/cases_eq.hlean
index f1f19806b..b2dc9c8cc 100644
--- a/tests/lean/hott/cases_eq.hlean
+++ b/tests/lean/hott/cases_eq.hlean
@@ -10,7 +10,7 @@ begin
   cases h₁, apply rfl
 end
 
-theorem congr {A B : Type} (f : A → B) {a₁ a₂ : A} (h : a₁ = a₂) : f a₁ = f a₂ :=
+theorem congr2 {A B : Type} (f : A → B) {a₁ a₂ : A} (h : a₁ = a₂) : f a₁ = f a₂ :=
 begin
   cases h, apply rfl
 end
diff --git a/tests/lean/hott/inj_tac.hlean b/tests/lean/hott/inj_tac.hlean
index 1b8be6c59..5e776fa76 100644
--- a/tests/lean/hott/inj_tac.hlean
+++ b/tests/lean/hott/inj_tac.hlean
@@ -1,5 +1,13 @@
-import data.vector
-open nat vector
+open nat
+
+inductive vector (A : Type) : nat → Type :=
+| nil {} : vector A zero
+| cons   : Π {n}, A → vector A n → vector A (succ n)
+
+open vector
+notation a :: b := cons a b
+notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
+
 
 example (a b : nat) : succ a = succ b → a + 2 = b + 2 :=
 begin
@@ -11,7 +19,7 @@ end
 example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) :
         a :: v = b :: w →  b = a :=
 begin
-  intro H, injection H with aeqb neqn beqw,
+  intro H, injection H with neqn aeqb beqw,
   rewrite aeqb
 end
 
diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean
index b8f0ebe99..a6b6df6a2 100644
--- a/tests/lean/run/tactic17.lean
+++ b/tests/lean/run/tactic17.lean
@@ -6,7 +6,7 @@ constant f : A → A → A
 
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c :=
 begin
-  apply (@congr A A _ _ (f a) (f b)),
+  apply (@congr A A (f a) (f b)),
   assumption,
   apply (congr_arg f),
   assumption