From 094459504b02fb2815ccb2a03d1be44304ff1c13 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 Aug 2014 13:27:18 -0700
Subject: [PATCH] fix(tests/lean/run): adjust test to changes in the library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/class1.lean        | 2 +-
 tests/lean/run/class2.lean        | 2 +-
 tests/lean/run/class3.lean        | 2 +-
 tests/lean/run/class6.lean        | 2 +-
 tests/lean/run/class8.lean        | 6 +++---
 tests/lean/run/congr_imp_bug.lean | 2 +-
 tests/lean/run/elab_bug1.lean     | 2 +-
 tests/lean/run/fun.lean           | 2 +-
 tests/lean/run/ptst.lean          | 2 +-
 9 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean
index aa25e295b..5c9627d83 100644
--- a/tests/lean/run/class1.lean
+++ b/tests/lean/run/class1.lean
@@ -1,5 +1,5 @@
 import standard
-using num pair
+using num prod
 
 definition H : inhabited (Prop × num × (num → num)) := _
 
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index 1f30dddff..eabfcade5 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -1,5 +1,5 @@
 import standard
-using num pair
+using num prod
 
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
 := _
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index 9c81dd297..e1547607f 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -1,5 +1,5 @@
 import standard
-using num pair
+using num prod
 
 section
   parameter {A : Type}
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index 9897342e8..274fe9147 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -1,5 +1,5 @@
 import standard
-using pair
+using prod
 
 inductive t1 : Type :=
 | mk1 : t1
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index 34956fe3c..6c99e4382 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -1,5 +1,5 @@
 import standard
-using num tactic pair
+using num tactic prod
 
 inductive inh (A : Type) : Prop :=
 | inh_intro : A -> inh A
@@ -18,8 +18,8 @@ theorem inh_bool [instance] : inh Prop
 theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B)
 := inh_rec (λb, inh_intro (λa : A, b)) H
 
-theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (pair A B)
-:= inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (mk_pair a b)))
+theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (prod A B)
+:= inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (pair a b)))
 
 definition assump := eassumption
 tactic_hint assump
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index c57f0a9f8..ab0c2f6e3 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
-import logic.connectives.basic logic.connectives.function
+import logic.connectives.basic struc.function
 using function
 
 namespace congr
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index 686f26d3b..860434555 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -4,7 +4,7 @@
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import standard
+import standard struc.function
 
 using function
 
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 2281e485e..fea5029f6 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -1,4 +1,4 @@
-import standard
+import standard struc.function
 using function num bool
 
 
diff --git a/tests/lean/run/ptst.lean b/tests/lean/run/ptst.lean
index d5a427de3..2537e4d46 100644
--- a/tests/lean/run/ptst.lean
+++ b/tests/lean/run/ptst.lean
@@ -1,5 +1,5 @@
 import standard
-using pair
+using prod
 
 -- Test tuple notation
 check (3, false, 1, true)