From 0c2e3656b3890176ca9e78fb3ecdf72edee86a53 Mon Sep 17 00:00:00 2001
From: puech
Date: Tue, 29 Nov 2011 14:28:31 +0000
Subject: Term: useless conversion to list in constr_ord deleted

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14738 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index d29f467a28..cb7bd7a998 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -613,10 +613,7 @@ let constr_ord_int f t1 t2 =
 	(f =? f) t1 t2 c1 c2
     | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
 	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (_,_), App (_,_) ->
-	let c1,l1=decompose_app t1
-	and c2,l2=decompose_app t2 in
-	  (f =? (list_compare f)) c1 c2 l1 l2
+    | App (c1,l1), App (c2,l2) -> (f =? (array_compare f)) c1 c2 l1 l2
     | Evar (e1,l1), Evar (e2,l2) ->
 	((-) =? (array_compare f)) e1 e2 l1 l2
     | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2)
-- 
cgit v1.2.3