aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Coloringaux.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-03-09 13:35:00 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-03-09 13:35:00 +0000
commit3ffda353b0d92ccd0ff3693ad0be81531c3c0537 (patch)
tree9a07da4e83919d763086e379de161fd4cfe8ab02 /backend/Coloringaux.ml
parent06c55ab8fa4c0bf59479faf03d30a51c780da36e (diff)
downloadcompcert-kvx-3ffda353b0d92ccd0ff3693ad0be81531c3c0537.tar.gz
compcert-kvx-3ffda353b0d92ccd0ff3693ad0be81531c3c0537.zip
Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Coloringaux.ml')
-rw-r--r--backend/Coloringaux.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 04209726..02081d56 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -169,13 +169,12 @@ end
module IntSet = Set.Make(struct
type t = int
- let compare x y =
- if x < y then -1 else if x > y then 1 else 0
+ let compare (x:int) (y:int) = compare x y
end)
module IntPairSet = Set.Make(struct
type t = int * int
- let compare (x1, y1) (x2, y2) =
+ let compare ((x1, y1): (int * int)) (x2, y2) =
if x1 < x2 then -1 else
if x1 > x2 then 1 else
if y1 < y2 then -1 else