diff options
| author | puech | 2011-08-01 13:46:34 +0000 |
|---|---|---|
| committer | puech | 2011-08-01 13:46:34 +0000 |
| commit | 0958a15e1c5a81c4ae3330ffd0b54923094962f6 (patch) | |
| tree | d7676c1ba43a2fcd8d078fac0dbd975436856380 /kernel | |
| parent | e9b7adf4709fe96ceece4b646fae2bea1e9b2085 (diff) | |
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
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 |