From 47e2247fe47dafe834855dd61e7b14b30c57f70d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Sun, 8 Mar 2015 19:27:09 +0100
Subject: ZArith/Int.v: some modernizations

---
 theories/MSets/MSetAVL.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'theories/MSets')

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index e1fc454ae..cc023cc3f 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -31,7 +31,7 @@
     code after extraction.
 *)
 
-Require Import MSetInterface MSetGenTree ZArith Int.
+Require Import MSetInterface MSetGenTree BinInt Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -83,11 +83,11 @@ Definition assert_false := create.
 Definition bal l x r :=
   let hl := height l in
   let hr := height r in
-  if gt_le_dec hl (hr+2) then
+  if (hr+2) <? hl then
     match l with
      | Leaf => assert_false l x r
      | Node _ ll lx lr =>
-       if ge_lt_dec (height ll) (height lr) then
+       if (height lr) <=? (height ll) then
          create ll lx (create lr x r)
        else
          match lr with
@@ -97,11 +97,11 @@ Definition bal l x r :=
          end
     end
   else
-    if gt_le_dec hr (hl+2) then
+    if (hl+2) <? hr then
       match r with
        | Leaf => assert_false l x r
        | Node _ rl rx rr =>
-         if ge_lt_dec (height rr) (height rl) then
+         if (height rl) <=? (height rr) then
             create (create l x rl) rx rr
          else
            match rl with
@@ -138,8 +138,8 @@ Fixpoint join l : elt -> t -> t :=
        fix join_aux (r:t) : t := match r with
           | Leaf => add x l
           | Node rh rl rx rr =>
-               if gt_le_dec lh (rh+2) then bal ll lx (join lr x r)
-               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr
+               if (rh+2) <? lh then bal ll lx (join lr x r)
+               else if (lh+2) <? rh then bal (join_aux rl) rx rr
                else create l x r
           end
   end.
@@ -419,12 +419,12 @@ Local Open Scope Int_scope.
 Ltac join_tac :=
  intro l; induction l as [| lh ll _ lx lr Hlr];
    [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join;
-     [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
+     [ | destruct ((rh+2) <? lh) eqn:LT;
        [ match goal with |- context b [ bal ?a ?b ?c] =>
            replace (bal a b c)
            with (bal ll lx (join lr x (Node rh rl rx rr))); [ | auto]
          end
-       | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
+       | destruct ((lh+2) <? rh) eqn:LT';
          [ match goal with |- context b [ bal ?a ?b ?c] =>
              replace (bal a b c)
              with (bal (join (Node lh ll lx lr) x rl) rx rr); [ | auto]
-- 
cgit v1.2.3