diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-01 22:56:50 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-01 22:56:50 +0000 |
| commit | 47ea85e784d83aabddcc9250bfe565833d1e4462 (patch) | |
| tree | c0019ea524a624db1496a7cc0c04ed09d999a9be /theories/FSets/FMapAVL.v | |
| parent | 1b7c478d62af9cc9d3da9ab8512d161be5028a13 (diff) | |
Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 2a2960f19..437f52ab0 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1592,11 +1592,11 @@ intros m; functional induction (map_option f m); simpl; auto; intros. inversion H. rewrite join_in in H; destruct H as [H|[H|H]]. exists d; split; auto; rewrite (f_compat d H), e0; discriminate. -destruct (IHt _ H) as {d0,?,?}; exists d0; auto. -destruct (IHt0 _ H) as {d0,?,?}; exists d0; auto. +destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto. +destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto. rewrite concat_in in H; destruct H as [H|H]. -destruct (IHt _ H) as {d0,?,?}; exists d0; auto. -destruct (IHt0 _ H) as {d0,?,?}; exists d0; auto. +destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto. +destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto. Qed. Lemma map_option_bst : forall m, bst m -> bst (map_option f m). @@ -1604,10 +1604,10 @@ Proof. intros m; functional induction (map_option f m); simpl; auto; intros; inv bst. apply join_bst; auto; intros y H; - destruct (map_option_2 H) as {d0,?,?}; eauto using MapsTo_In. + destruct (map_option_2 H) as (d0 & ? & ?); eauto using MapsTo_In. apply concat_bst; auto; intros y y' H H'. -destruct (map_option_2 H) as {d0,?,?}. -destruct (map_option_2 H') as {d0',?,?}. +destruct (map_option_2 H) as (d0 & ? & ?). +destruct (map_option_2 H') as (d0' & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed. Hint Resolve map_option_bst. @@ -1626,9 +1626,9 @@ intros m; functional induction (map_option f m); simpl; auto; intros; try destruct X.compare; simpl; auto. rewrite (f_compat d e); auto. intros y H; - destruct (map_option_2 H) as {?,?,?}; eauto using MapsTo_In. + destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. intros y H; - destruct (map_option_2 H) as {?,?,?}; eauto using MapsTo_In. + destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In. rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto. rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto. @@ -1637,8 +1637,8 @@ rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto. destruct (find x0 (map_option f r)); auto. intros y y' H H'. -destruct (map_option_2 H) as {?,?,?}. -destruct (map_option_2 H') as {?,?,?}. +destruct (map_option_2 H) as (? & ? & ?). +destruct (map_option_2 H') as (? & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed. |