From 666ca36470e7adad38bc775eb0062142fdcfd9bd Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Wed, 8 Mar 2017 21:41:04 -0500
Subject: [PATCH] fix(library/tests/lean/*): fix tests

---
 tests/lean/1369.lean                         | 4 ++--
 tests/lean/run/coe_univ_bug.lean             | 2 +-
 tests/lean/run/match2.lean                   | 2 +-
 tests/lean/run/pred_to_subtype_coercion.lean | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/lean/1369.lean b/tests/lean/1369.lean
index a932185544..31f17b8101 100644
--- a/tests/lean/1369.lean
+++ b/tests/lean/1369.lean
@@ -20,7 +20,7 @@ end
 
 example : { k : ℕ // k ≤ 555555 } :=
 begin
-  refine subtype.tag _ _,
+  refine subtype.mk _ _,
   exact 17,
   target >>= trace,
   trace_state,
@@ -32,7 +32,7 @@ set_option pp.instantiate_mvars false
 
 example : { k : ℕ // k ≤ 555555 } :=
 begin
-  refine subtype.tag _ _,
+  refine subtype.mk _ _,
   exact 17,
   target >>= trace,
   trace_state,
diff --git a/tests/lean/run/coe_univ_bug.lean b/tests/lean/run/coe_univ_bug.lean
index d947b33137..6921bced2a 100644
--- a/tests/lean/run/coe_univ_bug.lean
+++ b/tests/lean/run/coe_univ_bug.lean
@@ -12,7 +12,7 @@ instance pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
 ⟨Type u, (λ p : A → Prop, subtype p)⟩
 
 instance coesubtype {A : Type u} {p : A → Prop} : has_coe (@coe_sort _ pred2subtype p) A :=
-⟨λ s, subtype.elt_of s⟩
+⟨λ s, subtype.val s⟩
 
 def g {n : nat} (v : below n) : nat :=
 v + 1
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
index 2d8be25158..8ef703405c 100644
--- a/tests/lean/run/match2.lean
+++ b/tests/lean/run/match2.lean
@@ -4,4 +4,4 @@ inductive imf (f : nat → nat) : nat → Type
 
 definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat // x > b} → nat
 | .(f a)     (imf.mk1 .f a) x := a
-| .(f 0 + 1) (imf.mk2 .f)   x := subtype.elt_of x
+| .(f 0 + 1) (imf.mk2 .f)   x := subtype.val x
diff --git a/tests/lean/run/pred_to_subtype_coercion.lean b/tests/lean/run/pred_to_subtype_coercion.lean
index d9716ac190..b6bfcb70bb 100644
--- a/tests/lean/run/pred_to_subtype_coercion.lean
+++ b/tests/lean/run/pred_to_subtype_coercion.lean
@@ -18,4 +18,4 @@ sorry
 check f ⟨0, zlt10⟩
 
 definition g (a : below 10) : nat :=
-subtype.elt_of a
+subtype.val a