diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 22 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 2 |
4 files changed, 18 insertions, 18 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. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 671917595..209eb5497 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -1022,24 +1022,24 @@ Proof. induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; try discriminate H. (* p~1, q~1 *) - destruct (IHp q H) as {r,U,V,W}; exists (r~0); rewrite ?U, ?V; auto. + destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto. repeat split; auto; right. destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. rewrite ZL10; subst; auto. rewrite W; simpl; destruct r; auto; elim NE; auto. (* p~1, q~0 *) destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H. - destruct (IHp q H) as {r,U,V,W}; exists (r~1); rewrite ?U, ?V; auto. + destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto. exists 1; subst; rewrite Pminus_mask_diag; auto. (* p~1, 1 *) exists (p~0); auto. (* p~0, q~1 *) - destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as {r,U,V,W}. + destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W). destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto. exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto. (* p~0, q~0 *) - destruct (IHp q H) as {r,U,V,W}; exists (r~0); rewrite ?U, ?V; auto. + destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto. repeat split; auto; right. destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. rewrite ZL10; subst; auto. @@ -1052,7 +1052,7 @@ Qed. Theorem Pplus_minus : forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p. Proof. - intros p q H; destruct (Pminus_mask_Gt p q H) as {r,U,V,_}. + intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _). unfold Pminus; rewrite U; simpl; auto. Qed. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 591968a86..2996a5c91 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1876,7 +1876,7 @@ Section Int31_Spec. simpl tail031_alt. case_eq (firstr x); intros. rewrite (inj_S (tail031_alt n (shiftr x))), Zpower_Zsucc; auto with zarith. - destruct (IHn (shiftr x)) as {y,Hy1,Hy2}. + destruct (IHn (shiftr x)) as (y & Hy1 & Hy2). rewrite phi_nz; rewrite phi_nz in H; contradict H. rewrite (sneakl_shiftr x), H1, H; auto. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index de7e4c6e8..b439462db 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -806,7 +806,7 @@ Section ZModulo. clear; induction p. exists (Zpos p); simpl; rewrite Pmult_1_r; auto with zarith. - destruct IHp as {y,Yp,Ye}. + destruct IHp as (y & Yp & Ye). exists y. split; auto. change (Zpos p~0) with (2*Zpos p). |