diff options
| author | puech | 2011-11-29 14:28:31 +0000 |
|---|---|---|
| committer | puech | 2011-11-29 14:28:31 +0000 |
| commit | 0c2e3656b3890176ca9e78fb3ecdf72edee86a53 (patch) | |
| tree | eeb6fc81dc22cf94501bfa005e167384f1e492e5 /kernel/term.ml | |
| parent | 68fe6e8f354f4317decc5c69e2658fd17b5a5e90 (diff) | |
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
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 5 |
1 files changed, 1 insertions, 4 deletions
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) |