diff options
Diffstat (limited to 'theories/MSets/MSetAVL.v')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index e1fc454a..cc023cc3 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] |