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, 12 insertions, 12 deletions

diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index f792e4c2a7..d2c3e2776c 100755
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -12,17 +12,17 @@ Require Export Relation_Definitions.
 Require Export Relation_Operators.
 Require Export Operators_Properties.
 
-Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B)
-  (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))).
-Intros; Split; Elim H; Red; Auto.
-Intros _ equiv_trans _ x y z H0 H1; Apply equiv_trans with (f y); Assumption.
+Lemma inverse_image_of_equivalence :
+ forall (A B:Set) (f:A -> B) (r:relation B),
+   equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
+intros; split; elim H; red in |- *; auto.
+intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
-Lemma inverse_image_of_eq : (A,B:Set)(f:A->B)
-  (equivalence A [x,y:A](f x)=(f y)).
-Split; Red;
-[ (* reflexivity *)  Reflexivity
-| (* transitivity *) Intros; Transitivity (f y); Assumption
-| (* symmetry *) Intros; Symmetry; Assumption
-].
-Qed.
+Lemma inverse_image_of_eq :
+ forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+split; red in |- *;
+ [  (* reflexivity *) reflexivity
+ |  (* transitivity *) intros; transitivity (f y); assumption
+ |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+Qed.
\ No newline at end of file