diff options
| author | Vincent Laporte | 2019-10-10 12:14:55 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-22 06:38:20 +0000 |
| commit | abdf4058321e3767421cd0c30d8f4fc63e0518e3 (patch) | |
| tree | 0ba1d02ef366ee5901f4f8fc4554bb54f607e567 | |
| parent | f0014b4c9bbfa840c952b8943934056a7b0a446e (diff) | |
FSets: do not use “omega”
| -rw-r--r-- | theories/FSets/FMapAVL.v | 3 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 4 |
3 files changed, 5 insertions, 4 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 7c69350db4..ea4062d9fe 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1363,7 +1363,8 @@ Lemma elements_aux_cardinal : Proof. simple induction m; simpl; intuition. rewrite <- H; simpl. - rewrite <- H0; omega. + rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc. + reflexivity. Qed. Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m). diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 0ef356b582..fa553d9fce 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -68,7 +68,7 @@ Hint Constructors avl : core. Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0. Proof. - induction s; simpl; intros; auto with zarith. + induction s; simpl; intros. now apply Z.le_ge. inv avl; intuition; omega_max. Qed. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index e5133f66b2..342a51b39b 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. unfold elements. intros m; set (p:=1); clearbody p; revert m p. induction m; simpl; auto; intros. - rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto. - destruct o; rewrite app_length; simpl; omega. + rewrite (IHm1 (append p 2)), (IHm2 (append p 3)). + destruct o; rewrite app_length; simpl; auto. Qed. End CompcertSpec. |