From 0958a15e1c5a81c4ae3330ffd0b54923094962f6 Mon Sep 17 00:00:00 2001
From: puech
Date: Mon, 1 Aug 2011 13:46:34 +0000
Subject: Term: simplify compare_constr by removing calls to decompose_app

I think the additional check was here for historical reasons (before the invariant on Apps was enforced)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14379 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index 15e461308d..99a0e6bb3b 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -563,14 +563,8 @@ let compare_constr f t1 t2 =
   | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
   | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
   | App (c1,l1), App (c2,l2) ->
-      if Array.length l1 = Array.length l2 then
-        f c1 c2 & array_for_all2 f l1 l2
-      else
-        let (h1,l1) = decompose_app t1 in
-        let (h2,l2) = decompose_app t2 in
-        if List.length l1 = List.length l2 then
-          f h1 h2 & List.for_all2 f l1 l2
-        else false
+    Array.length l1 = Array.length l2 &&
+      f c1 c2 && array_for_all2 f l1 l2
   | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
   | Const c1, Const c2 -> eq_constant c1 c2
   | Ind c1, Ind c2 -> eq_ind c1 c2
-- 
cgit v1.2.3