diff options
Diffstat (limited to 'theories/MSets')
-rw-r--r-- | theories/MSets/MSetGenTree.v | 6 | ||||
-rw-r--r-- | theories/MSets/MSetRBT.v | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 320ced06c..901574235 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -27,7 +27,7 @@ - min_elt max_elt choose *) -Require Import Orders OrdersFacts MSetInterface NPeano. +Require Import Orders OrdersFacts MSetInterface PeanoNat. Local Open Scope list_scope. Local Open Scope lazy_bool_scope. @@ -1129,14 +1129,14 @@ Proof. Qed. Lemma maxdepth_log_cardinal s : s <> Leaf -> - log2 (cardinal s) < maxdepth s. + Nat.log2 (cardinal s) < maxdepth s. Proof. intros H. apply Nat.log2_lt_pow2. destruct s; simpl; intuition. apply maxdepth_cardinal. Qed. -Lemma mindepth_log_cardinal s : mindepth s <= log2 (S (cardinal s)). +Lemma mindepth_log_cardinal s : mindepth s <= Nat.log2 (S (cardinal s)). Proof. apply Nat.log2_le_pow2. auto with arith. apply mindepth_cardinal. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index b79afc616..af67aa1ec 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -31,7 +31,7 @@ Additional suggested reading: *) Require MSetGenTree. -Require Import Bool List BinPos Pnat Setoid SetoidList NPeano. +Require Import Bool List BinPos Pnat Setoid SetoidList PeanoNat. Local Open Scope list_scope. (* For nicer extraction, we create induction principles @@ -1566,7 +1566,7 @@ Proof. Qed. Lemma maxdepth_upperbound s : Rbt s -> - maxdepth s <= 2 * log2 (S (cardinal s)). + maxdepth s <= 2 * Nat.log2 (S (cardinal s)). Proof. intros (n,H). eapply Nat.le_trans; [eapply rb_maxdepth; eauto|]. @@ -1581,7 +1581,7 @@ Proof. Qed. Lemma maxdepth_lowerbound s : s<>Leaf -> - log2 (cardinal s) < maxdepth s. + Nat.log2 (cardinal s) < maxdepth s. Proof. apply maxdepth_log_cardinal. Qed. |