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, 36 insertions, 38 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 8a5a9892a..0051c4e00 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -13,61 +13,59 @@ Section Setoid.
 Variable A : Type.
 Variable Aeq : A -> A -> Prop.
 
-Record Setoid_Theory : Prop :=
-{ Seq_refl : (x:A) (Aeq x x);
-  Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x);
-  Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z)
-}.
+Record Setoid_Theory : Prop := 
+  {Seq_refl : forall x:A, Aeq x x;
+   Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
+   Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z}.
 
 End Setoid.
 
-Definition Prop_S : (Setoid_Theory Prop iff).
-Split; [Exact iff_refl | Exact iff_sym | Exact iff_trans].
+Definition Prop_S : Setoid_Theory Prop iff.
+split; [ exact iff_refl | exact iff_sym | exact iff_trans ].
 Qed.
 
 Add Setoid Prop iff Prop_S.
 
-Hint prop_set : setoid := Resolve (Seq_refl Prop iff Prop_S).
-Hint prop_set : setoid := Resolve (Seq_sym Prop iff Prop_S).
-Hint prop_set : setoid := Resolve (Seq_trans Prop iff Prop_S).
+Hint Resolve (Seq_refl Prop iff Prop_S): setoid.
+Hint Resolve (Seq_sym Prop iff Prop_S): setoid.
+Hint Resolve (Seq_trans Prop iff Prop_S): setoid.
 
 Add Morphism or : or_ext.
-Intros.
-Inversion H1.
-Left.
-Inversion H.
-Apply (H3 H2).
-
-Right.
-Inversion H0.
-Apply (H3 H2).
+intros.
+inversion H1.
+left.
+inversion H.
+apply (H3 H2).
+
+right.
+inversion H0.
+apply (H3 H2).
 Qed.
 
 Add Morphism and : and_ext.
-Intros.
-Inversion H1.
-Split.
-Inversion H.
-Apply (H4 H2).
-
-Inversion H0.
-Apply (H4 H3).
+intros.
+inversion H1.
+split.
+inversion H.
+apply (H4 H2).
+
+inversion H0.
+apply (H4 H3).
 Qed.
 
 Add Morphism not : not_ext.
-Red ; Intros.
-Apply H0.
-Inversion H.
-Apply (H3 H1).
+red in |- *; intros.
+apply H0.
+inversion H.
+apply (H3 H1).
 Qed.
 
-Definition fleche [A,B:Prop] := A -> B.
+Definition fleche (A B:Prop) := A -> B.
 
 Add Morphism fleche : fleche_ext.
-Unfold fleche.
-Intros.
-Inversion H0.
-Inversion H.
-Apply (H3 (H1 (H6 H2))).
+unfold fleche in |- *.
+intros.
+inversion H0.
+inversion H.
+apply (H3 (H1 (H6 H2))).
 Qed.
-