From 2aa64034dfda5c63050781e88698f7633a20aae5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jun 2015 17:10:18 -0700
Subject: [PATCH] fix(tests/lean): adjust tests to reflect changes in the
 elaboration process

---
 tests/lean/531.hlean              | 14 --------------
 tests/lean/531.hlean.expected.out |  2 +-
 tests/lean/hott/329.hlean         |  4 +---
 tests/lean/hott/615.hlean         |  2 +-
 tests/lean/run/nested_rec.lean    |  3 +--
 5 files changed, 4 insertions(+), 21 deletions(-)

diff --git a/tests/lean/531.hlean b/tests/lean/531.hlean
index b7e210f15..e867d51a0 100644
--- a/tests/lean/531.hlean
+++ b/tests/lean/531.hlean
@@ -134,18 +134,4 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
     }
   end
 
-example
-{P : pushout → Type}
-{Pinl : Π (x : BL), P (inl x)}
-{Pinr : Π (x : TR), P (inr x)}
-{Pglue : Π (x : TL), eq (transport (λ (x : pushout), P x) (glue x) (Pinl (f x))) (Pinr (g x))}
-{y : pushout}
-{x : @ob _ (@dom _ tt)}
-: eq (transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))
-    (Pinl (f x)) :=
-begin
-rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}con_tr,
-apply sorry
-end
-
 exit
diff --git a/tests/lean/531.hlean.expected.out b/tests/lean/531.hlean.expected.out
index c70917a50..44d406145 100644
--- a/tests/lean/531.hlean.expected.out
+++ b/tests/lean/531.hlean.expected.out
@@ -1 +1 @@
-531.hlean:151:0: warning: using 'exit' to interrupt Lean
+531.hlean:137:0: warning: using 'exit' to interrupt Lean
diff --git a/tests/lean/hott/329.hlean b/tests/lean/hott/329.hlean
index 51654fc41..9c5b0170f 100644
--- a/tests/lean/hott/329.hlean
+++ b/tests/lean/hott/329.hlean
@@ -7,9 +7,7 @@ definition path_sigma_dpair (p : a = a') (q : p ▸ b = b') : sigma.mk a b = sig
 eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
 
 definition path_sigma (p :  pr1 u = pr1 v) (q : p ▸ pr2 u = pr2 v) : u = v :=
-destruct u
-         (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
-         p q
+begin cases u, cases v, apply path_sigma_dpair p q end
 
 definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : p1 ▸ b = b'}
     (s : idp ▸ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 :=
diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean
index 128910e8e..74c5d0c1a 100644
--- a/tests/lean/hott/615.hlean
+++ b/tests/lean/hott/615.hlean
@@ -16,5 +16,5 @@ protected definition my_decode {x : circle} : my_code x → base = x :=
     induction x,
     { exact power loop},
     { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
-      rewrite [power_con,transport_code_loop]},
+      xrewrite [power_con, transport_code_loop]},
   end
diff --git a/tests/lean/run/nested_rec.lean b/tests/lean/run/nested_rec.lean
index f0b146647..ba9a6c6eb 100644
--- a/tests/lean/run/nested_rec.lean
+++ b/tests/lean/run/nested_rec.lean
@@ -29,8 +29,7 @@ theorem g_succ (a : nat) : g (succ a) = g (g a) :=
 have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from
   well_founded.fix_eq g.F (succ a),
 calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl
-          ...   = pr₁ (sigma.mk (g (g a)) _)          : {aux}
-          ...   = g (g a)                              : rfl
+          ...   = g (g a)                             : {aux}
 
 theorem g_all_zero (a : nat) : g a = zero :=
 nat.induction_on a