diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
| commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
| tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /theories/Sets/Classical_sets.v | |
| parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) | |
Kills the useless tactic annotations "in |- *"
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets/Classical_sets.v')
| -rw-r--r-- | theories/Sets/Classical_sets.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index f93631c7e..bf7b52b22 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -38,8 +38,8 @@ Section Ensembles_classical. elim (not_all_ex_not U (fun x:U => ~ In U A x)). intros x H; apply Inhabited_intro with x. apply NNPP; auto with sets. - red in |- *; intro. - apply NI; red in |- *. + red; intro. + apply NI; red. intros x H'; elim (H x); trivial with sets. Qed. @@ -47,7 +47,7 @@ Section Ensembles_classical. forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. Proof. intros; apply not_included_empty_Inhabited. - red in |- *; auto with sets. + red; auto with sets. Qed. Lemma Inhabited_Setminus : @@ -73,7 +73,7 @@ Section Ensembles_classical. Lemma Subtract_intro : forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. Proof. - unfold Subtract at 1 in |- *; auto with sets. + unfold Subtract at 1; auto with sets. Qed. Hint Resolve Subtract_intro : sets. @@ -103,7 +103,7 @@ Section Ensembles_classical. Lemma not_SIncl_empty : forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). Proof. - intro X; red in |- *; intro H'; try exact H'. + intro X; red; intro H'; try exact H'. lapply (Strict_Included_inv X (Empty_set U)); auto with sets. intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. intros x H'0; elim H'0. @@ -113,10 +113,10 @@ Section Ensembles_classical. Lemma Complement_Complement : forall A:Ensemble U, Complement U (Complement U A) = A. Proof. - unfold Complement in |- *; intros; apply Extensionality_Ensembles; + unfold Complement; intros; apply Extensionality_Ensembles; auto with sets. - red in |- *; split; auto with sets. - red in |- *; intros; apply NNPP; auto with sets. + red; split; auto with sets. + red; intros; apply NNPP; auto with sets. Qed. End Ensembles_classical. |