diff options
Diffstat (limited to 'theories/FSets/FMapAVL.v')
-rw-r--r-- | theories/FSets/FMapAVL.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index bee922c6f..7f5853494 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1270,10 +1270,10 @@ Proof. inv bst. rewrite H2, join_find; auto; clear H2. - simpl; destruct X.compare; simpl; auto. + simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. - apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto. + apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto. intros z Hz; apply H1; auto; rewrite H3; auto. Qed. @@ -1622,8 +1622,8 @@ Lemma map_option_find : forall (m:t elt)(x:key), Proof. intros m; functional induction (map_option f m); simpl; auto; intros; inv bst; rewrite join_find || rewrite concat_find; auto; simpl; - try destruct X.compare; simpl; auto. -rewrite (f_compat d e); auto. + try destruct X.compare as [Hlt|Heq|Hlt]; simpl; auto. +rewrite (f_compat d Heq); auto. intros y H; destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. intros y H; @@ -1631,7 +1631,7 @@ intros y H; rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto. -rewrite (f_compat d e); auto. +rewrite (f_compat d Heq); auto. rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto. destruct (find x0 (map_option f r)); auto. |