aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-01 22:56:50 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-01 22:56:50 +0000
commit47ea85e784d83aabddcc9250bfe565833d1e4462 (patch)
treec0019ea524a624db1496a7cc0c04ed09d999a9be /theories/FSets
parent1b7c478d62af9cc9d3da9ab8512d161be5028a13 (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')
-rw-r--r--theories/FSets/FMapAVL.v22
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.