From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- theories/MSets/MSetList.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/MSets/MSetList.v') diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index bcf68f1d..d9b1fd9b 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -662,7 +662,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction s; simpl; intros. split; intuition; inv. - destruct (f a) as [ ]_eqn:F; rewrite !InA_cons, ?IHs; intuition. + destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition. setoid_replace x with a; auto. setoid_replace a with x in F; auto; congruence. Qed. @@ -674,7 +674,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. unfold For_all; induction s; simpl; intros. split; intros; auto. inv. - destruct (f a) as [ ]_eqn:F. + destruct (f a) eqn:F. rewrite IHs; auto. firstorder. inv; auto. setoid_replace x with a; auto. split; intros H'. discriminate. @@ -688,7 +688,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. unfold Exists; induction s; simpl; intros. firstorder. discriminate. inv. - destruct (f a) as [ ]_eqn:F. + destruct (f a) eqn:F. firstorder. rewrite IHs; auto. firstorder. -- cgit v1.2.3