diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 10 |
1 files changed, 2 insertions, 8 deletions
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 |