From 7ab5e72794d564d0b8550bb06a832d44793d36fc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 2 Jan 2009 17:24:46 +0000
Subject: Conséquence renommage canonique de refl_equal en eq_refl.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11736 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Cases.out | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 1f0e12d3f7..1ec02c56a5 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