diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-03 17:54:30 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-03 17:54:30 +0000 |
| commit | b432ebcdf0f76a6b25956b696601fe8a06fa4638 (patch) | |
| tree | f58d0d0ba6d2e61d378926d48e7a25ffaf1772af /kernel/term.ml | |
| parent | d5b13126177a7f30069d0512f1d08b34e00e3fee (diff) | |
Removing two Pervasives.compare from Term.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 1a829c3a4..82d534a33 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -628,6 +628,9 @@ let constr_ord_int f t1 t2 = let (==?) fg h i1 i2 j1 j2 k1 k2= let c=fg i1 i2 j1 j2 in if Int.equal c 0 then h k1 k2 else c in + let fix_cmp (a1, i1) (a2, i2) = + ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2 + in match kind_of_term t1, kind_of_term t2 with | Rel n1, Rel n2 -> Int.compare n1 n2 | Meta m1, Meta m2 -> Int.compare m1 m2 @@ -651,10 +654,10 @@ let constr_ord_int f t1 t2 = | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (Array.compare f)) ==? (Array.compare f)) + ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (Array.compare f)) ==? (Array.compare f)) + ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | t1, t2 -> Pervasives.compare t1 t2 |