Merge branch 'experimental/upstream' into upstream

1 files changed, 15 insertions, 17 deletions

diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 372473d6..cdbeaf7b 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,8 +24,6 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Ensembles.
 Require Export Relations_1.
 Require Export Relations_1_facts.
@@ -41,7 +39,7 @@ Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
 Hint Resolve Definition_of_Power_set.
 
 Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
-intro X; red in |- *.
+intro X; red.
 intros x H'; elim H'.
 Qed.
 Hint Resolve Empty_set_minimal.
@@ -81,7 +79,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion :
    Strict_Included U x y -> Included U y z -> Strict_Included U x z.
 intros x y z H' H'0; try assumption.
 elim Strict_Rel_is_Strict_Included.
-unfold contains in |- *.
+unfold contains.
 intros H'1 H'2; try assumption.
 apply H'1.
 apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets.
@@ -92,7 +90,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion_left :
    Included U x y -> Strict_Included U y z -> Strict_Included U x z.
 intros x y z H' H'0; try assumption.
 elim Strict_Rel_is_Strict_Included.
-unfold contains in |- *.
+unfold contains.
 intros H'1 H'2; try assumption.
 apply H'1.
 apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets.
@@ -107,14 +105,14 @@ Qed.
 
 Theorem Empty_set_is_Bottom :
  forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
-intro A; apply Bottom_definition; simpl in |- *; auto with sets.
+intro A; apply Bottom_definition; simpl; auto with sets.
 Qed.
 Hint Resolve Empty_set_is_Bottom.
 
 Theorem Union_minimal :
  forall a b X:Ensemble U,
    Included U a X -> Included U b X -> Included U (Union U a b) X.
-intros a b X H' H'0; red in |- *.
+intros a b X H' H'0; red.
 intros x H'1; elim H'1; auto with sets.
 Qed.
 Hint Resolve Union_minimal.
@@ -135,13 +133,13 @@ Qed.
 
 Theorem Intersection_decreases_l :
  forall a b:Ensemble U, Included U (Intersection U a b) a.
-intros a b; red in |- *.
+intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
 
 Theorem Intersection_decreases_r :
  forall a b:Ensemble U, Included U (Intersection U a b) b.
-intros a b; red in |- *.
+intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
 Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
@@ -153,10 +151,10 @@ Theorem Union_is_Lub :
    Included U b A ->
    Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
 intros A a b H' H'0.
-apply Lub_definition; simpl in |- *.
-apply Upper_Bound_definition; simpl in |- *; auto with sets.
+apply Lub_definition; simpl.
+apply Upper_Bound_definition; simpl; auto with sets.
 intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; simpl; auto with sets.
 Qed.
 
 Theorem Intersection_is_Glb :
@@ -166,13 +164,13 @@ Theorem Intersection_is_Glb :
    Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b)
      (Intersection U a b).
 intros A a b H' H'0.
-apply Glb_definition; simpl in |- *.
-apply Lower_Bound_definition; simpl in |- *; auto with sets.
+apply Glb_definition; simpl.
+apply Lower_Bound_definition; simpl; auto with sets.
 apply Definition_of_Power_set.
 generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
  auto with sets.
 intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; simpl; auto with sets.
 Qed.
 
 End The_power_set_partial_order.
@@ -187,4 +185,4 @@ Hint Resolve Union_increases_r: sets v62.
 Hint Resolve Intersection_decreases_l: sets v62.
 Hint Resolve Intersection_decreases_r: sets v62.
 Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62.
\ No newline at end of file
+Hint Resolve Strict_inclusion_is_transitive: sets v62.