From fb81bcaeee3d5090913d053090c3cf301dc826f8 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 23 Jun 2016 23:26:37 +0100
Subject: [PATCH] fix(tests): fix tests after changes is the HoTT library

---
 tests/lean/extra/616b.hlean    | 2 +-
 tests/lean/extra/616c.hlean    | 2 +-
 tests/lean/extra/755.hlean     | 2 +-
 tests/lean/hott/ind_tac1.hlean | 1 +
 4 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/tests/lean/extra/616b.hlean b/tests/lean/extra/616b.hlean
index 7416663be..6f6a3ae8d 100644
--- a/tests/lean/extra/616b.hlean
+++ b/tests/lean/extra/616b.hlean
@@ -5,5 +5,5 @@ definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P)
 begin
   induction x,
     exact (Pc a),
-    refine (pathover_of_eq (Pp H))
+    refine (pathover_of_eq _ (Pp H))
 end
diff --git a/tests/lean/extra/616c.hlean b/tests/lean/extra/616c.hlean
index cbb536dbf..2ddee3855 100644
--- a/tests/lean/extra/616c.hlean
+++ b/tests/lean/extra/616c.hlean
@@ -4,5 +4,5 @@ definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P)
 begin
   induction x,
     exact (Pc a),
-    refine (pathover_of_eq (Pp H))
+    refine (pathover_of_eq _ (Pp H))
 end
diff --git a/tests/lean/extra/755.hlean b/tests/lean/extra/755.hlean
index 2df1b7cd0..959cb9b98 100644
--- a/tests/lean/extra/755.hlean
+++ b/tests/lean/extra/755.hlean
@@ -27,7 +27,7 @@ section
 
   protected definition elim {P : Type} (Pt : A → P)
     (Pe : Π(a a' : A), Pt a = Pt a') (x : one_step_tr) : P :=
-  rec Pt (λa a', pathover_of_eq (Pe a a')) x
+  rec Pt (λa a', pathover_of_eq _ (Pe a a')) x
 
   theorem rec_tr_eq {P : one_step_tr → Type} (Pt : Π(a : A), P (tr a))
     (Pe : Π(a a' : A), Pt a =[tr_eq a a'] Pt a') (a a' : A)
diff --git a/tests/lean/hott/ind_tac1.hlean b/tests/lean/hott/ind_tac1.hlean
index 9155edd92..ceef2aab9 100644
--- a/tests/lean/hott/ind_tac1.hlean
+++ b/tests/lean/hott/ind_tac1.hlean
@@ -1,3 +1,4 @@
+open eq
 set_option pp.universes true
 
 check @homotopy.rec_on