From fde83cd376b17ee70c69cc42e09bf7218c6d754e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Mar 2015 09:28:16 -0800
Subject: [PATCH] fix(tests/lean/hott): adjust tests to reflect changes in the
 libraries

---
 tests/lean/hott/443.hlean                     | 4 ++--
 tests/lean/interactive/in2.input.expected.out | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/lean/hott/443.hlean b/tests/lean/hott/443.hlean
index 4109a0ee4..61b0a2895 100644
--- a/tests/lean/hott/443.hlean
+++ b/tests/lean/hott/443.hlean
@@ -1,6 +1,6 @@
-import algebra.group algebra.precategory.basic algebra.precategory.morphism
+import algebra.group algebra.precategory.basic
 
-open eq sigma unit category morphism path_algebra
+open eq sigma unit category path_algebra
 
 context
   parameters {P₀ : Type} [P : precategory P₀]
diff --git a/tests/lean/interactive/in2.input.expected.out b/tests/lean/interactive/in2.input.expected.out
index 0e82394e0..11093a4e5 100644
--- a/tests/lean/interactive/in2.input.expected.out
+++ b/tests/lean/interactive/in2.input.expected.out
@@ -9,5 +9,5 @@ Type₁ : Type₂
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINEVAL
-tst.foo.{l_2 l_1} : ?A → ?B → ?A
+tst.foo.{l_1 l_2} : ?A → ?B → ?A
 -- ENDEVAL