From 24f78632d7ec81c3f2675168de7e0987d42685df Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 3 Nov 2001 16:33:06 +0000
Subject: interversion de deux Elim dans In_dec pour que la fonction extraite
 soit efficace

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2156 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/PolyList.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 0a6d05956f..40af3d16e0 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -240,7 +240,8 @@ Lemma In_dec : ((x,y:A){x=y}+{~x=y}) ->   (a:A)(l:list){(In a l)}+{~(In a l)}.
 Proof.
   Induction l.
   Right; Apply in_nil.
-  Intros; Elim H0; Simpl; Elim (H a0 a); Auto.
+  Intros; Elim (H a0 a); Simpl; Auto.
+  Elim H0; Simpl; Auto. 
   Right; Unfold not; Intros [Hc1 | Hc2]; Auto.
 Save.
 
-- 
cgit v1.2.3