Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 71 insertions, 74 deletions

diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 78ad3d2f2..b4250be92 100755
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -29,134 +29,131 @@
 Require Export Ensembles.
 
 Section Ensembles_facts.
-Variable U: Type.
+Variable U : Type.
 
-Lemma Extension: (B, C: (Ensemble U)) B == C -> (Same_set U B C).
+Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
 Proof.
-Intros B C H'; Rewrite H'; Auto with sets.
+intros B C H'; rewrite H'; auto with sets.
 Qed.
 
-Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x).
+Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
 Proof.
-Red; NewDestruct 1.
+red in |- *; destruct 1.
 Qed.
-Hints Resolve Noone_in_empty.
+Hint Resolve Noone_in_empty.
 
-Lemma Included_Empty: (A: (Ensemble U))(Included U (Empty_set U) A).
+Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
 Proof.
-Intro; Red.
-Intros x H; Elim (Noone_in_empty x); Auto with sets.
+intro; red in |- *.
+intros x H; elim (Noone_in_empty x); auto with sets.
 Qed.
-Hints Resolve Included_Empty.
+Hint Resolve Included_Empty.
 
-Lemma Add_intro1:
-  (A: (Ensemble U)) (x, y: U) (In U A y) -> (In U (Add U A x) y).
+Lemma Add_intro1 :
+ forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
 Proof.
-Unfold 1 Add; Auto with sets.
+unfold Add at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Add_intro1.
+Hint Resolve Add_intro1.
 
-Lemma Add_intro2: (A: (Ensemble U)) (x: U) (In U (Add U A x) x).
+Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
 Proof.
-Unfold 1 Add; Auto with sets.
+unfold Add at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Add_intro2.
+Hint Resolve Add_intro2.
 
-Lemma Inhabited_add: (A: (Ensemble U)) (x: U) (Inhabited U (Add U A x)).
+Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
 Proof.
-Intros A x.
-Apply Inhabited_intro with x := x; Auto with sets.
+intros A x.
+apply Inhabited_intro with (x := x); auto with sets.
 Qed.
-Hints Resolve Inhabited_add.
+Hint Resolve Inhabited_add.
 
-Lemma Inhabited_not_empty:
-  (X: (Ensemble U)) (Inhabited U X) -> ~ X == (Empty_set U).
+Lemma Inhabited_not_empty :
+ forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
 Proof.
-Intros X H'; Elim H'.
-Intros x H'0; Red; Intro H'1.
-Absurd (In U X x); Auto with sets.
-Rewrite H'1; Auto with sets.
+intros X H'; elim H'.
+intros x H'0; red in |- *; intro H'1.
+absurd (In U X x); auto with sets.
+rewrite H'1; auto with sets.
 Qed.
-Hints Resolve Inhabited_not_empty.
+Hint Resolve Inhabited_not_empty.
 
-Lemma Add_not_Empty :
- (A: (Ensemble U)) (x: U) ~ (Add U A x) == (Empty_set U).
+Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
-Hints Resolve Add_not_Empty.
+Hint Resolve Add_not_Empty.
 
-Lemma not_Empty_Add :
- (A: (Ensemble U)) (x: U) ~ (Empty_set U) == (Add U A x).
+Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
 Proof.
-Intros; Red; Intro H; Generalize (Add_not_Empty A x); Auto with sets.
+intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
 Qed.
-Hints Resolve not_Empty_Add.
+Hint Resolve not_Empty_Add.
 
-Lemma Singleton_inv: (x, y: U) (In U (Singleton U x) y) -> x == y.
+Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
 Proof.
-Intros x y H'; Elim H'; Trivial with sets.
+intros x y H'; elim H'; trivial with sets.
 Qed.
-Hints Resolve Singleton_inv.
+Hint Resolve Singleton_inv.
 
-Lemma Singleton_intro: (x, y: U) x == y -> (In U (Singleton U x) y).
+Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
 Proof.
-Intros x y H'; Rewrite H'; Trivial with sets.
+intros x y H'; rewrite H'; trivial with sets.
 Qed.
-Hints Resolve Singleton_intro.
+Hint Resolve Singleton_intro.
 
-Lemma Union_inv:  (B, C: (Ensemble U)) (x: U) 
-  (In U (Union U B C) x) -> (In U B x) \/ (In U C x).
+Lemma Union_inv :
+ forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
 Proof.
-Intros B C x H'; Elim H'; Auto with sets.
+intros B C x H'; elim H'; auto with sets.
 Qed.
 
-Lemma Add_inv:
-  (A: (Ensemble U)) (x, y: U) (In U (Add U A x) y) -> (In U A y) \/ x == y.
+Lemma Add_inv :
+ forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
 Proof.
-Intros A x y H'; Elim H'; Auto with sets.
+intros A x y H'; elim H'; auto with sets.
 Qed.
 
-Lemma Intersection_inv:
-  (B, C: (Ensemble U)) (x: U) (In U (Intersection U B C) x) ->
-   (In U B x) /\ (In U C x).
+Lemma Intersection_inv :
+ forall (B C:Ensemble U) (x:U),
+   In U (Intersection U B C) x -> In U B x /\ In U C x.
 Proof.
-Intros B C x H'; Elim H'; Auto with sets.
+intros B C x H'; elim H'; auto with sets.
 Qed.
-Hints Resolve Intersection_inv.
+Hint Resolve Intersection_inv.
 
-Lemma Couple_inv: (x, y, z: U) (In U (Couple U x y) z) -> z == x \/ z == y.
+Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
 Proof.
-Intros x y z H'; Elim H'; Auto with sets.
+intros x y z H'; elim H'; auto with sets.
 Qed.
-Hints Resolve Couple_inv.
+Hint Resolve Couple_inv.
 
-Lemma Setminus_intro:
-  (A, B: (Ensemble U)) (x: U) (In U A x) -> ~ (In U B x) ->
-   (In U (Setminus U A B) x).
+Lemma Setminus_intro :
+ forall (A B:Ensemble U) (x:U),
+   In U A x -> ~ In U B x -> In U (Setminus U A B) x.
 Proof.
-Unfold 1 Setminus; Red; Auto with sets.
+unfold Setminus at 1 in |- *; red in |- *; auto with sets.
 Qed.
-Hints Resolve Setminus_intro.
+Hint Resolve Setminus_intro.
  
-Lemma Strict_Included_intro:
-  (X, Y: (Ensemble U)) (Included U X Y) /\ ~ X == Y -> 
-                       (Strict_Included U X Y).
+Lemma Strict_Included_intro :
+ forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
-Hints Resolve Strict_Included_intro.
+Hint Resolve Strict_Included_intro.
 
-Lemma Strict_Included_strict: (X: (Ensemble U)) ~ (Strict_Included U X X).
+Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
 Proof.
-Intro X; Red; Intro H'; Elim H'.
-Intros H'0 H'1; Elim H'1; Auto with sets.
+intro X; red in |- *; intro H'; elim H'.
+intros H'0 H'1; elim H'1; auto with sets.
 Qed.
-Hints Resolve Strict_Included_strict.
+Hint Resolve Strict_Included_strict.
 
 End Ensembles_facts.
 
-Hints Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 
-	Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
-	Strict_Included_strict Noone_in_empty Inhabited_not_empty
-	Add_not_Empty  not_Empty_Add Inhabited_add Included_Empty : sets v62.
+Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
+  Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
+  Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
+  not_Empty_Add Inhabited_add Included_Empty: sets v62.
\ No newline at end of file