From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/output/Cases.out | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'test-suite/output/Cases.out')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 1f0e12d3..1ec02c56 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -9,10 +9,9 @@ fix F (t : t) : P t :=
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match eq_nat_dec x y with
-| left eqprf =>
-    match eqprf in (_ = z) return (P z) with
-    | refl_equal => def
-    end
+| left eqprf => match eqprf in (_ = z) return (P z) with
+                | eq_refl => def
+                end
 | right _ => prf
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-- 
cgit v1.2.3