From 20539d698f0c6a317b9f85981dfec545d9dfa1ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Oct 2015 15:33:45 -0700
Subject: [PATCH] fix(tests/lean): tests affected by new type class resolution
 procedure

---
 tests/lean/binder_overload.lean.expected.out      |  4 ++--
 tests/lean/finset_induction_bug.lean.expected.out |  8 ++++----
 tests/lean/namespace_bug.lean                     |  2 +-
 tests/lean/namespace_bug.lean.expected.out        |  9 +--------
 tests/lean/unique_instances.lean                  | 10 ----------
 tests/lean/unique_instances.lean.expected.out     |  4 ----
 6 files changed, 8 insertions(+), 29 deletions(-)
 delete mode 100644 tests/lean/unique_instances.lean
 delete mode 100644 tests/lean/unique_instances.lean.expected.out

diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out
index 56929e9dc..340154fe8 100644
--- a/tests/lean/binder_overload.lean.expected.out
+++ b/tests/lean/binder_overload.lean.expected.out
@@ -1,7 +1,7 @@
 {x : ℕ ∈ S | x > 0} : set ℕ
 {x : ℕ ∈ s | x > 0} : finset ℕ
 @set.sep.{1} nat (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) S : set.{1} nat
-@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0)
-  (λ (a : nat), nat.decidable_lt 0 a)
+@finset.sep.{1} nat (λ (x x_1 : nat), nat.has_decidable_eq x x_1) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0)
+  (λ (x : nat), nat.decidable_lt 0 x)
   s :
   finset.{1} nat
diff --git a/tests/lean/finset_induction_bug.lean.expected.out b/tests/lean/finset_induction_bug.lean.expected.out
index 53e651aa6..434ff9801 100644
--- a/tests/lean/finset_induction_bug.lean.expected.out
+++ b/tests/lean/finset_induction_bug.lean.expected.out
@@ -22,12 +22,12 @@ l' : list A,
 IH : ∀ (x : @nodup A l'), P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' x)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
-H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
+H3 : @eq (list A) (@list.insert A (λ (x x_1 : A), h x x_1) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
 P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
 H4 :
   P
-    (@insert A (λ (a b : A), h a b) a
+    (@insert A (λ (x x_1 : A), h x x_1) a
        (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
 ⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:30:45: error: don't know how to synthesize placeholder
@@ -44,12 +44,12 @@ l' : list A,
 IH : ∀ (x : @nodup A l'), P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' x)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
-H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
+H3 : @eq (list A) (@list.insert A (λ (x x_1 : A), h x x_1) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
 P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
 H4 :
   P
-    (@insert A (λ (a b : A), h a b) a
+    (@insert A (λ (x x_1 : A), h x x_1) a
        (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
 ⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:16:5: error: failed to add declaration 'finset.induction₂' to environment, value has metavariables
diff --git a/tests/lean/namespace_bug.lean b/tests/lean/namespace_bug.lean
index 32059d1fe..0ddb03c0f 100644
--- a/tests/lean/namespace_bug.lean
+++ b/tests/lean/namespace_bug.lean
@@ -1,5 +1,5 @@
 namespace playground
 namespace nat
-check 2+3 -- Should produce error
+check 2+3
 end nat
 end playground
diff --git a/tests/lean/namespace_bug.lean.expected.out b/tests/lean/namespace_bug.lean.expected.out
index 48d80bcbb..fe2b5863c 100644
--- a/tests/lean/namespace_bug.lean.expected.out
+++ b/tests/lean/namespace_bug.lean.expected.out
@@ -1,8 +1 @@
-namespace_bug.lean:3:6: error: type mismatch at application
-  @bit0 ?A
-term
-  ?A
-has type
-  Type.{l_2}
-but is expected to have type
-  Type.{l_3}
+2 + 3 : ?A
diff --git a/tests/lean/unique_instances.lean b/tests/lean/unique_instances.lean
deleted file mode 100644
index e929b8cd6..000000000
--- a/tests/lean/unique_instances.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import logic data.prod
-open prod
-
-set_option class.unique_instances true set_option pp.implicit true
-theorem tst (A : Type) (H₁ : inhabited A) (H₂ : inhabited A) : inhabited (A × A) :=
-_
-
-set_option class.unique_instances false
-theorem tst2 (A : Type) (H₁ : inhabited A) (H₂ : inhabited A) : inhabited (A × A) :=
-_
diff --git a/tests/lean/unique_instances.lean.expected.out b/tests/lean/unique_instances.lean.expected.out
deleted file mode 100644
index c494cf5bb..000000000
--- a/tests/lean/unique_instances.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-unique_instances.lean:6:0: error: ambiguous class-instance resolution, there is more than one solution
-  @prod.is_inhabited A A H₂ H₂
-and
-  @prod.is_inhabited A A H₂ H₁