diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-03-08 19:27:09 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-02 11:44:18 +0200 |
commit | 47e2247fe47dafe834855dd61e7b14b30c57f70d (patch) | |
tree | efe7c096c10d22ad7b409398e6a2be89a1525e56 /theories/MSets | |
parent | c356a3b01a428504f66f027802b7b19f0761203e (diff) |
ZArith/Int.v: some modernizations
Diffstat (limited to 'theories/MSets')
-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 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] |