let cmp x y =
  let domcmp d e =
    match d, e with
      | None, None -> 0
      | Some _, None -> -1
      | None, Some _ -> 1
      | Some d, Some e ->
          (match d, e with   
             | Dom.Real, Dom.Real -> 0
             | Dom.Int, Dom.Int -> 0
             | Dom.Real, Dom.Int -> 1    (* real-valued variables are larger *)
             | Dom.Int, Dom.Real -> -1)
  in 
  let strictcmp alpha beta =    
    match alpha, beta with
      | true, false -> -1           (* nonstrict slacks are smaller *)
      | false, true -> 1
      | _ -> 0
  in
    match x, y with
      | External _, Rename _ -> -1   (* external variables are smaller than renaming vars. *)
      | Rename _, External _ -> 1
      | External(n, d), External(m, e) -> 
          let c1 = domcmp d e in
            if c1 != 0 then c1 else Name.cmp n m
      | Rename(n, i, d), Rename(m, j, e) -> 
          let c1 = domcmp d e in
            if c1 != 0 then c1 else 
              let c2 = Name.cmp n m  in
                if c2 != 0 then c2 else Pervasives.compare i j
      | Fresh(n, i, d), Fresh(m, j, e) -> 
          let c1 = domcmp d e in
            if c1 != 0 then c1 else 
              let c2 = Name.cmp n m  in
                if c2 != 0 then c2 else Pervasives.compare i j
      | Slack(i, alpha, d), Slack(j, beta, e) ->  
          let c1 = strictcmp alpha beta in
            if c1 != 0 then c1 else 
              let c2 = domcmp d e in   (* newer slack vars are smaller *)
                if c2 != 0 then c2 else -(Pervasives.compare i j)
      | Slack _, _ -> -1           (* slacks are smaller than other variables. *)
      | _, Slack _ -> 1
      | External _, Fresh _ -> 1   (* external variables are larger than fresh vars *)
      | Fresh _, External _ -> -1
      | Bound(n), Bound(m) -> 
          Pervasives.compare n m
      | _ -> 
          Pervasives.compare x y