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

6 files changed, 297 insertions, 277 deletions

diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 57e93240a..7de49f62f 100755
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -8,108 +8,116 @@
 
 (*i $Id$ i*)
 
-Require Rstar.
+Require Import Rstar.
 
 Section Newman.
 
-Variable A: Type. 
-Variable R: A->A->Prop.
+Variable A : Type. 
+Variable R : A -> A -> Prop.
 
-Local Rstar := (Rstar A R). 
-Local Rstar_reflexive := (Rstar_reflexive A R).
-Local Rstar_transitive := (Rstar_transitive A R).
-Local Rstar_Rstar' := (Rstar_Rstar' A R).
+Let Rstar := Rstar A R. 
+Let Rstar_reflexive := Rstar_reflexive A R.
+Let Rstar_transitive := Rstar_transitive A R.
+Let Rstar_Rstar' := Rstar_Rstar' A R.
 
-Definition coherence := [x:A][y:A] (exT2 ? (Rstar x) (Rstar y)).
+Definition coherence (x y:A) := ex2 (Rstar x) (Rstar y).
 
-Theorem coherence_intro :  (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y).
-Proof [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)]
-      (exT_intro2 A (Rstar x) (Rstar y) z h1 h2).
+Theorem coherence_intro :
+ forall x y z:A, Rstar x z -> Rstar y z -> coherence x y.
+Proof
+  fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) =>
+    ex_intro2 (Rstar x) (Rstar y) z h1 h2.
   
 (** A very simple case of coherence : *)
 
-Lemma Rstar_coherence : (x:A)(y:A)(Rstar x y)->(coherence x y).
- Proof  [x:A][y:A][h:(Rstar x y)](coherence_intro x y y h (Rstar_reflexive y)).  
+Lemma Rstar_coherence : forall x y:A, Rstar x y -> coherence x y.
+ Proof
+   fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y).  
   
 (** coherence is symmetric *)
-Lemma coherence_sym: (x:A)(y:A)(coherence x y)->(coherence y x).
- Proof [x:A][y:A][h:(coherence x y)]
-        (exT2_ind A (Rstar x) (Rstar y) (coherence y x)
-                 [w:A][h1:(Rstar x w)][h2:(Rstar y w)]
-                      (coherence_intro y x w h2 h1) h).
-
-Definition confluence :=
-     [x:A](y:A)(z:A)(Rstar x y)->(Rstar x z)->(coherence y z).  
+Lemma coherence_sym : forall x y:A, coherence x y -> coherence y x.
+ Proof
+   fun (x y:A) (h:coherence x y) =>
+     ex2_ind
+       (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) =>
+          coherence_intro y x w h2 h1) h.
+
+Definition confluence (x:A) :=
+  forall y z:A, Rstar x y -> Rstar x z -> coherence y z.  
   
-Definition local_confluence :=
-     [x:A](y:A)(z:A)(R x y)->(R x z)->(coherence y z).  
+Definition local_confluence (x:A) :=
+  forall y z:A, R x y -> R x z -> coherence y z.  
   
 Definition noetherian :=
-     (x:A)(P:A->Prop)((y:A)((z:A)(R y z)->(P z))->(P y))->(P x).  
+  forall (x:A) (P:A -> Prop),
+    (forall y:A, (forall z:A, R y z -> P z) -> P y) -> P x.  
   
 Section Newman_section.
 
 (** The general hypotheses of the theorem *)
 
-Hypothesis Hyp1:noetherian.
-Hypothesis Hyp2:(x:A)(local_confluence x).  
+Hypothesis Hyp1 : noetherian.
+Hypothesis Hyp2 : forall x:A, local_confluence x.  
   
 (** The induction hypothesis *)
 
 Section Induct.
-  Variable    x:A.
-  Hypothesis  hyp_ind:(u:A)(R x u)->(confluence u).  
+  Variable x : A.
+  Hypothesis hyp_ind : forall u:A, R x u -> confluence u.  
   
 (** Confluence in [x] *)
 
-  Variables   y,z:A.  
-  Hypothesis  h1:(Rstar x y).  
-  Hypothesis  h2:(Rstar x z).  
+  Variables y z : A.  
+  Hypothesis h1 : Rstar x y.  
+  Hypothesis h2 : Rstar x z.  
   
 (** particular case [x->u] and [u->*y]   *)
 Section Newman_.
-  Variable    u:A.  
-  Hypothesis  t1:(R x u).  
-  Hypothesis  t2:(Rstar u y).  
+  Variable u : A.  
+  Hypothesis t1 : R x u.  
+  Hypothesis t2 : Rstar u y.  
   
 (** In the usual diagram, we assume also [x->v] and [v->*z] *)
 
-Theorem Diagram : (v:A)(u1:(R x v))(u2:(Rstar v z))(coherence y z).
-
-Proof     (* We draw the diagram ! *)
-   [v:A][u1:(R x v)][u2:(Rstar v z)]
-   (exT2_ind A (Rstar u) (Rstar v)    (* local confluence in x for u,v *)
-      (coherence y z)                (* gives w, u->*w and v->*w *)
-      ([w:A][s1:(Rstar u w)][s2:(Rstar v w)]
-   (exT2_ind A (Rstar y) (Rstar w)    (* confluence in u => coherence(y,w) *)
-      (coherence y z)                (* gives a, y->*a and z->*a *)
-      ([a:A][v1:(Rstar y a)][v2:(Rstar w a)]
-   (exT2_ind A (Rstar a) (Rstar z)    (* confluence in v => coherence(a,z) *)
-      (coherence y z)                (* gives b, a->*b and z->*b *)
-      ([b:A][w1:(Rstar a b)][w2:(Rstar z b)]
-        (coherence_intro y z b (Rstar_transitive y a b v1 w1) w2))
-      (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2)))
-     (hyp_ind u t1 y w t2 s1)))
-    (Hyp2 x u v t1 u1)).
+Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z.
+
+Proof
+   (* We draw the diagram ! *)
+  fun (v:A) (u1:R x v) (u2:Rstar v z) =>
+    ex2_ind
+       (* local confluence in x for u,v *)
+       (* gives w, u->*w and v->*w *)
+      (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) =>
+         ex2_ind
+            (* confluence in u => coherence(y,w) *)
+            (* gives a, y->*a and z->*a *)
+           (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) =>
+              ex2_ind
+                 (* confluence in v => coherence(a,z) *)
+                 (* gives b, a->*b and z->*b *)
+                (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) =>
+                   coherence_intro y z b (Rstar_transitive y a b v1 w1) w2)
+                (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2))
+           (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1).
   
-Theorem caseRxy : (coherence y z).
-Proof (Rstar_Rstar' x z h2 
-      ([v:A][w:A](coherence y w))
-      (coherence_sym x y (Rstar_coherence x y h1))  (*i case x=z i*)
-      Diagram).                                     (*i case x->v->*z i*)
+Theorem caseRxy : coherence y z.
+Proof
+  Rstar_Rstar' x z h2 (fun v w:A => coherence y w)
+    (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*)
+    Diagram.                                     (*i case x->v->*z i*)
 End Newman_.
 
-Theorem Ind_proof : (coherence y z).
-Proof (Rstar_Rstar' x y h1 ([u:A][v:A](coherence v z))
-        (Rstar_coherence x z h2)                    (*i case x=y i*)
-        caseRxy).                                   (*i case x->u->*z i*)
+Theorem Ind_proof : coherence y z.
+Proof
+  Rstar_Rstar' x y h1 (fun u v:A => coherence v z)
+    (Rstar_coherence x z h2) (*i case x=y i*)
+    caseRxy.                                   (*i case x->u->*z i*)
 End Induct.
 
-Theorem Newman : (x:A)(confluence x).
-Proof [x:A](Hyp1 x confluence Ind_proof).  
+Theorem Newman : forall x:A, confluence x.
+Proof fun x:A => Hyp1 x confluence Ind_proof.  
 
 End Newman_section.
 
 
 End Newman.
-
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 0ca819b84..9534f707f 100755
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -12,55 +12,53 @@
 (*                            Bruno Barras                                  *)
 (****************************************************************************)
 
-Require Relation_Definitions.
-Require Relation_Operators.
+Require Import Relation_Definitions.
+Require Import Relation_Operators.
 
 
 Section Properties.
 
-  Variable A: Set.
-  Variable R: (relation A).
+  Variable A : Set.
+  Variable R : relation A.
 
-  Local incl : (relation A)->(relation A)->Prop :=
-      [R1,R2: (relation A)] (x,y:A) (R1 x y) -> (R2 x y).
+  Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
 
 Section Clos_Refl_Trans.
 
-  Lemma clos_rt_is_preorder: (preorder A (clos_refl_trans A R)).
-Apply Build_preorder.
-Exact (rt_refl A R).
+  Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R).
+apply Build_preorder.
+exact (rt_refl A R).
 
-Exact (rt_trans A R).
+exact (rt_trans A R).
 Qed.
 
 
 
-Lemma clos_rt_idempotent:
-       (incl (clos_refl_trans A (clos_refl_trans A R))
-                     (clos_refl_trans A R)).
-Red.
-NewInduction 1; Auto with sets.
-Intros.
-Apply rt_trans with y; Auto with sets.
+Lemma clos_rt_idempotent :
+ incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R).
+red in |- *.
+induction 1; auto with sets.
+intros.
+apply rt_trans with y; auto with sets.
 Qed.
 
-  Lemma  clos_refl_trans_ind_left: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop)
-           (P M)
-            ->((P0,N:A)
-                (clos_refl_trans A R M P0)->(P P0)->(R P0 N)->(P N))
-               ->(a:A)(clos_refl_trans A R M a)->(P a).
-Intros.
-Generalize H H0 .
-Clear  H H0.
-Elim H1; Intros; Auto with sets.
-Apply H2 with x; Auto with sets.
-
-Apply H3.
-Apply H0; Auto with sets.
-
-Intros.
-Apply H5 with P0; Auto with sets.
-Apply rt_trans with y; Auto with sets.
+  Lemma clos_refl_trans_ind_left :
+   forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
+     P M ->
+     (forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
+     forall a:A, clos_refl_trans A R M a -> P a.
+intros.
+generalize H H0.
+clear H H0.
+elim H1; intros; auto with sets.
+apply H2 with x; auto with sets.
+
+apply H3.
+apply H0; auto with sets.
+
+intros.
+apply H5 with P0; auto with sets.
+apply rt_trans with y; auto with sets.
 Qed.
 
 
@@ -69,30 +67,30 @@ End Clos_Refl_Trans.
 
 Section Clos_Refl_Sym_Trans.
 
-  Lemma clos_rt_clos_rst: (inclusion A (clos_refl_trans A R)
-				        (clos_refl_sym_trans A R)).
-Red.
-NewInduction 1; Auto with sets.
-Apply rst_trans with y; Auto with sets.
+  Lemma clos_rt_clos_rst :
+   inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R).
+red in |- *.
+induction 1; auto with sets.
+apply rst_trans with y; auto with sets.
 Qed.
 
-  Lemma clos_rst_is_equiv: (equivalence A (clos_refl_sym_trans A R)).
-Apply Build_equivalence.
-Exact (rst_refl A R).
+  Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R).
+apply Build_equivalence.
+exact (rst_refl A R).
 
-Exact (rst_trans A R).
+exact (rst_trans A R).
 
-Exact (rst_sym A R).
+exact (rst_sym A R).
 Qed.
 
-  Lemma clos_rst_idempotent:
-       (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
-                     (clos_refl_sym_trans A R)).
-Red.
-NewInduction 1; Auto with sets.
-Apply rst_trans with y; Auto with sets.
+  Lemma clos_rst_idempotent :
+   incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
+     (clos_refl_sym_trans A R).
+red in |- *.
+induction 1; auto with sets.
+apply rst_trans with y; auto with sets.
 Qed.
 
 End Clos_Refl_Sym_Trans.
 
-End Properties.
+End Properties.
\ No newline at end of file
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 32f433d07..06440fd86 100755
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -10,19 +10,19 @@
 
 Section Relation_Definition.
 
-   Variable A: Type.
+   Variable A : Type.
    
-   Definition relation :=  A -> A -> Prop.
+   Definition relation := A -> A -> Prop.
 
-   Variable R: relation.
+   Variable R : relation.
    
 
 Section General_Properties_of_Relations.
 
-  Definition reflexive : Prop :=  (x: A) (R x x).
-  Definition transitive : Prop :=  (x,y,z: A) (R x y) -> (R y z) -> (R x z).
-  Definition symmetric : Prop :=  (x,y: A) (R x y) -> (R y x).
-  Definition antisymmetric : Prop :=  (x,y: A) (R x y) -> (R y x) -> x=y.
+  Definition reflexive : Prop := forall x:A, R x x.
+  Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.
+  Definition symmetric : Prop := forall x y:A, R x y -> R y x.
+  Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y.
 
   (* for compatibility with Equivalence in  ../PROGRAMS/ALG/  *)
   Definition equiv := reflexive /\ transitive /\ symmetric.
@@ -33,23 +33,20 @@ End General_Properties_of_Relations.
 
 Section Sets_of_Relations.
 
-   Record preorder : Prop := {
-       preord_refl  : reflexive;
-       preord_trans : transitive }.
+   Record preorder : Prop := 
+     {preord_refl : reflexive; preord_trans : transitive}.
 
-   Record order : Prop := {
-       ord_refl    : reflexive;
-       ord_trans   : transitive;
-       ord_antisym : antisymmetric }.
+   Record order : Prop := 
+     {ord_refl : reflexive;
+      ord_trans : transitive;
+      ord_antisym : antisymmetric}.
 
-   Record equivalence : Prop := {
-       equiv_refl  : reflexive;
-       equiv_trans : transitive;
-       equiv_sym   : symmetric }.
+   Record equivalence : Prop := 
+     {equiv_refl : reflexive;
+      equiv_trans : transitive;
+      equiv_sym : symmetric}.
    
-   Record PER : Prop := {
-       per_sym   : symmetric;
-       per_trans : transitive }.
+   Record PER : Prop :=  {per_sym : symmetric; per_trans : transitive}.
 
 End Sets_of_Relations.
 
@@ -57,27 +54,25 @@ End Sets_of_Relations.
 
 Section Relations_of_Relations.
 
-  Definition inclusion : relation -> relation -> Prop :=
-      [R1,R2: relation] (x,y:A) (R1 x y) -> (R2 x y).
+  Definition inclusion (R1 R2:relation) : Prop :=
+    forall x y:A, R1 x y -> R2 x y.
 
-  Definition same_relation : relation -> relation -> Prop :=
-      [R1,R2: relation] (inclusion R1 R2) /\ (inclusion R2 R1).
+  Definition same_relation (R1 R2:relation) : Prop :=
+    inclusion R1 R2 /\ inclusion R2 R1.
    
-  Definition commut : relation -> relation -> Prop :=
-      [R1,R2:relation] (x,y:A) (R1 y x) -> (z:A) (R2 z y)
-                          -> (EX y':A |(R2 y' x) & (R1 z y')).
+  Definition commut (R1 R2:relation) : Prop :=
+    forall x y:A,
+      R1 y x -> forall z:A, R2 z y ->  exists2 y' : A | R2 y' x & R1 z y'.
 
 End Relations_of_Relations.
 
    
 End Relation_Definition.
 
-Hints Unfold reflexive transitive antisymmetric symmetric : sets v62.
+Hint Unfold reflexive transitive antisymmetric symmetric: sets v62.
 
-Hints Resolve Build_preorder Build_order Build_equivalence 
-	Build_PER preord_refl preord_trans 
-	ord_refl ord_trans ord_antisym
-	equiv_refl equiv_trans equiv_sym
-	per_sym per_trans : sets v62.
+Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
+  preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
+  equiv_trans equiv_sym per_sym per_trans: sets v62.
 
-Hints Unfold inclusion same_relation commut : sets v62.
+Hint Unfold inclusion same_relation commut: sets v62.
\ No newline at end of file
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 7b07ac0db..0d5f2fd97 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -16,72 +16,76 @@
 (*     L. Paulson  JSC (1986) 2, 325-355                                    *)
 (****************************************************************************)
 
-Require Relation_Definitions.
-Require PolyList.
-Require PolyListSyntax.
+Require Import Relation_Definitions.
+Require Import List.
 
 (** Some operators to build relations *)
 
 Section Transitive_Closure.
-  Variable A: Set.
-  Variable R: (relation A).
+  Variable A : Set.
+  Variable R : relation A.
 
-  Inductive clos_trans : A->A->Prop :=
-     t_step: (x,y:A)(R x y)->(clos_trans x y)
-   | t_trans: (x,y,z:A)(clos_trans x y)->(clos_trans y z)->(clos_trans x z).
+  Inductive clos_trans : A -> A -> Prop :=
+    | t_step : forall x y:A, R x y -> clos_trans x y
+    | t_trans :
+        forall x y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
 End Transitive_Closure.
 
 
 Section Reflexive_Transitive_Closure.
-  Variable A: Set.
-  Variable R: (relation A).
-
-  Inductive clos_refl_trans: (relation A) :=
-    rt_step: (x,y:A)(R x y)->(clos_refl_trans x y)
-  | rt_refl: (x:A)(clos_refl_trans x x)
-  | rt_trans: (x,y,z: A)(clos_refl_trans x y)->(clos_refl_trans y z)
-                      ->(clos_refl_trans x z).
+  Variable A : Set.
+  Variable R : relation A.
+
+  Inductive clos_refl_trans : relation A :=
+    | rt_step : forall x y:A, R x y -> clos_refl_trans x y
+    | rt_refl : forall x:A, clos_refl_trans x x
+    | rt_trans :
+        forall x y z:A,
+          clos_refl_trans x y -> clos_refl_trans y z -> clos_refl_trans x z.
 End Reflexive_Transitive_Closure.
 
 
 Section Reflexive_Symetric_Transitive_Closure.
-  Variable A: Set.
-  Variable R: (relation A).
-
-  Inductive clos_refl_sym_trans: (relation A) :=
-    rst_step: (x,y:A)(R x y)->(clos_refl_sym_trans x y)
-  | rst_refl: (x:A)(clos_refl_sym_trans x x)
-  | rst_sym: (x,y:A)(clos_refl_sym_trans x y)->(clos_refl_sym_trans y x)
-  | rst_trans: (x,y,z:A)(clos_refl_sym_trans x y)->(clos_refl_sym_trans y z)
-                      ->(clos_refl_sym_trans x z).
+  Variable A : Set.
+  Variable R : relation A.
+
+  Inductive clos_refl_sym_trans : relation A :=
+    | rst_step : forall x y:A, R x y -> clos_refl_sym_trans x y
+    | rst_refl : forall x:A, clos_refl_sym_trans x x
+    | rst_sym :
+        forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x
+    | rst_trans :
+        forall x y z:A,
+          clos_refl_sym_trans x y ->
+          clos_refl_sym_trans y z -> clos_refl_sym_trans x z.
 End Reflexive_Symetric_Transitive_Closure.
 
 
 Section Transposee.
-  Variable A: Set.
-  Variable R: (relation A).
+  Variable A : Set.
+  Variable R : relation A.
 
-  Definition transp := [x,y:A](R y x).
+  Definition transp (x y:A) := R y x.
 End Transposee.
 
 
 Section Union.
-  Variable A: Set.
-  Variable R1,R2: (relation A).
+  Variable A : Set.
+  Variables R1 R2 : relation A.
 
-  Definition union := [x,y:A](R1 x y)\/(R2 x y).
+  Definition union (x y:A) := R1 x y \/ R2 x y.
 End Union.
 
 
 Section Disjoint_Union.
-Variable A,B:Set.
-Variable leA: A->A->Prop.
-Variable leB: B->B->Prop.
+Variables A B : Set.
+Variable leA : A -> A -> Prop.
+Variable leB : B -> B -> Prop.
 
-Inductive le_AsB : A+B->A+B->Prop :=
-   le_aa: (x,y:A) (leA x y) -> (le_AsB (inl A B x) (inl A B y))
-|  le_ab: (x:A)(y:B) (le_AsB (inl A B x) (inr A B y))
-|  le_bb: (x,y:B)  (leB x y) -> (le_AsB (inr A B x) (inr A B y)).
+Inductive le_AsB : A + B -> A + B -> Prop :=
+  | le_aa : forall x y:A, leA x y -> le_AsB (inl B x) (inl B y)
+  | le_ab : forall (x:A) (y:B), le_AsB (inl B x) (inr A y)
+  | le_bb : forall x y:B, leB x y -> le_AsB (inr A x) (inr A y).
 
 End Disjoint_Union. 
 
@@ -90,68 +94,74 @@ End Disjoint_Union.
 Section Lexicographic_Product.
 (* Lexicographic order on dependent pairs *)
 
-Variable A:Set.
-Variable B:A->Set.
-Variable leA: A->A->Prop.
-Variable leB: (x:A)(B x)->(B x)->Prop.
-
-Inductive lexprod : (sigS A B) -> (sigS A B) ->Prop :=
-  left_lex : (x,x':A)(y:(B x)) (y':(B x')) 
-               (leA x x') ->(lexprod (existS A B x y) (existS A B x' y'))
-| right_lex : (x:A) (y,y':(B x)) 
-                (leB x y y') -> (lexprod (existS A B x y) (existS A B x y')).
+Variable A : Set.
+Variable B : A -> Set.
+Variable leA : A -> A -> Prop.
+Variable leB : forall x:A, B x -> B x -> Prop.
+
+Inductive lexprod : sigS B -> sigS B -> Prop :=
+  | left_lex :
+      forall (x x':A) (y:B x) (y':B x'),
+        leA x x' -> lexprod (existS B x y) (existS B x' y')
+  | right_lex :
+      forall (x:A) (y y':B x),
+        leB x y y' -> lexprod (existS B x y) (existS B x y').
 End Lexicographic_Product.
 
 
 Section Symmetric_Product.
-  Variable A:Set.
-  Variable B:Set.
-  Variable leA: A->A->Prop.
-  Variable leB: B->B->Prop.
+  Variable A : Set.
+  Variable B : Set.
+  Variable leA : A -> A -> Prop.
+  Variable leB : B -> B -> Prop.
 
-  Inductive symprod : (A*B) -> (A*B) ->Prop :=
-     left_sym : (x,x':A)(leA x x')->(y:B)(symprod (x,y) (x',y))
-  | right_sym : (y,y':B)(leB y y')->(x:A)(symprod (x,y) (x,y')).
+  Inductive symprod : A * B -> A * B -> Prop :=
+    | left_sym :
+        forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y)
+    | right_sym :
+        forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y').
 
 End Symmetric_Product.
 
 
 Section Swap.
-  Variable A:Set.
-  Variable R:A->A->Prop.
-
-  Inductive swapprod: (A*A)->(A*A)->Prop :=
-     sp_noswap: (x,x':A*A)(symprod A A R R x x')->(swapprod x x')
-   | sp_swap: (x,y:A)(p:A*A)(symprod A A R R (x,y) p)->(swapprod (y,x) p).
+  Variable A : Set.
+  Variable R : A -> A -> Prop.
+
+  Inductive swapprod : A * A -> A * A -> Prop :=
+    | sp_noswap : forall x x':A * A, symprod A A R R x x' -> swapprod x x'
+    | sp_swap :
+        forall (x y:A) (p:A * A),
+          symprod A A R R (x, y) p -> swapprod (y, x) p.
 End Swap.
 
 
 Section Lexicographic_Exponentiation.
 
 Variable A : Set.
-Variable leA : A->A->Prop.
-Local Nil := (nil A).
-Local List := (list A).
+Variable leA : A -> A -> Prop.
+Let Nil := nil (A:=A).
+Let List := list A.
 
-Inductive Ltl : List->List->Prop :=
-  Lt_nil: (a:A)(x:List)(Ltl Nil (cons a x))
-| Lt_hd : (a,b:A) (leA a b)-> (x,y:(list A))(Ltl (cons a x) (cons b y))
-| Lt_tl : (a:A)(x,y:List)(Ltl x y) -> (Ltl (cons a x) (cons a y)).
+Inductive Ltl : List -> List -> Prop :=
+  | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x)
+  | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
+  | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y).
 
 
-Inductive Desc : List->Prop :=
-   d_nil : (Desc Nil)
-|  d_one : (x:A)(Desc (cons x Nil))
-|  d_conc : (x,y:A)(l:List)(leA x y) 
-              -> (Desc l^(cons y Nil))->(Desc (l^(cons y Nil))^(cons x Nil)).
+Inductive Desc : List -> Prop :=
+  | d_nil : Desc Nil
+  | d_one : forall x:A, Desc (x :: Nil)
+  | d_conc :
+      forall (x y:A) (l:List),
+        leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
-Definition  Pow :Set := (sig List Desc).
+Definition Pow : Set := sig Desc.
 
-Definition lex_exp : Pow -> Pow ->Prop := 
-      [a,b:Pow](Ltl (proj1_sig List Desc a) (proj1_sig  List Desc b)).
+Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b).
 
 End Lexicographic_Exponentiation.
 
-Hints Unfold transp union : sets v62.
-Hints Resolve t_step rt_step rt_refl rst_step rst_refl : sets v62.
-Hints Immediate rst_sym : sets v62.
+Hint Unfold transp union: sets v62.
+Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62.
+Hint Immediate rst_sym: sets v62.
\ No newline at end of file
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index f792e4c2a..d2c3e2776 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
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index 90ab6d6c2..349650629 100755
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -13,66 +13,75 @@
 Section Rstar.
 
 Variable A : Type.  
-Variable R : A->A->Prop.  
+Variable R : A -> A -> Prop.  
 
 (** Definition of the reflexive-transitive closure [R*] of [R] *)
 (** Smallest reflexive [P] containing [R o P] *)
 
-Definition Rstar  := [x,y:A](P:A->A->Prop)
-   ((u:A)(P u u))->((u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)) -> (P x y).  
+Definition Rstar (x y:A) :=
+  forall P:A -> A -> Prop,
+    (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y.  
 
-Theorem Rstar_reflexive:  (x:A)(Rstar x x).
- Proof [x:A][P:A->A->Prop]
-       [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)]
-       (h1 x).  
+Theorem Rstar_reflexive : forall x:A, Rstar x x.
+ Proof
+   fun (x:A) (P:A -> A -> Prop) (h1:forall u:A, P u u)
+     (h2:forall u v w:A, R u v -> P v w -> P u w) => 
+     h1 x.  
   
-Theorem Rstar_R: (x:A)(y:A)(z:A)(R x y)->(Rstar y z)->(Rstar x z).
- Proof [x:A][y:A][z:A][t1:(R x y)][t2:(Rstar y z)]
-       [P:A->A->Prop]
-       [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)]
-       (h2 x y z t1 (t2 P h1 h2)).  
+Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z.
+ Proof
+   fun (x y z:A) (t1:R x y) (t2:Rstar y z) (P:A -> A -> Prop)
+     (h1:forall u:A, P u u) (h2:forall u v w:A, R u v -> P v w -> P u w) =>
+     h2 x y z t1 (t2 P h1 h2).  
   
 (** We conclude with transitivity of [Rstar] : *)
 
-Theorem  Rstar_transitive:  (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z).
- Proof  [x:A][y:A][z:A][h:(Rstar x y)]
-        (h ([u:A][v:A](Rstar v z)->(Rstar u z))
-           ([u:A][t:(Rstar u z)]t)
-           ([u:A][v:A][w:A][t1:(R u v)][t2:(Rstar w z)->(Rstar v z)]
-            [t3:(Rstar w z)](Rstar_R u v z t1 (t2 t3)))).  
+Theorem Rstar_transitive :
+ forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z.
+ Proof
+   fun (x y z:A) (h:Rstar x y) =>
+     h (fun u v:A => Rstar v z -> Rstar u z) (fun (u:A) (t:Rstar u z) => t)
+       (fun (u v w:A) (t1:R u v) (t2:Rstar w z -> Rstar v z)
+          (t3:Rstar w z) => Rstar_R u v z t1 (t2 t3)).  
 
 (** Another characterization of [R*] *)
 (** Smallest reflexive [P] containing [R o R*] *)
 
-Definition Rstar' := [x:A][y:A](P:A->A->Prop)
-    ((P x x))->((u:A)(R x u)->(Rstar u y)->(P x y)) -> (P x y).  
+Definition Rstar' (x y:A) :=
+  forall P:A -> A -> Prop,
+    P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y.  
 
-Theorem Rstar'_reflexive: (x:A)(Rstar' x x).
- Proof  [x:A][P:A->A->Prop][h:(P x x)][h':(u:A)(R x u)->(Rstar u x)->(P x x)]h.
+Theorem Rstar'_reflexive : forall x:A, Rstar' x x.
+ Proof
+   fun (x:A) (P:A -> A -> Prop) (h:P x x)
+     (h':forall u:A, R x u -> Rstar u x -> P x x) => h.
   
-Theorem Rstar'_R: (x:A)(y:A)(z:A)(R x z)->(Rstar z y)->(Rstar' x y).
- Proof  [x:A][y:A][z:A][t1:(R x z)][t2:(Rstar z y)]
-        [P:A->A->Prop][h1:(P x x)]
-        [h2:(u:A)(R x u)->(Rstar u y)->(P x y)](h2 z t1 t2).  
+Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y.
+ Proof
+   fun (x y z:A) (t1:R x z) (t2:Rstar z y) (P:A -> A -> Prop) 
+     (h1:P x x) (h2:forall u:A, R x u -> Rstar u y -> P x y) => 
+     h2 z t1 t2.  
   
 (** Equivalence of the two definitions: *)
 
-Theorem Rstar'_Rstar:  (x:A)(y:A)(Rstar' x y)->(Rstar x y).
- Proof  [x:A][y:A][h:(Rstar' x y)]
-        (h Rstar (Rstar_reflexive x) ([u:A](Rstar_R x u y))).  
+Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y.
+ Proof
+   fun (x y:A) (h:Rstar' x y) =>
+     h Rstar (Rstar_reflexive x) (fun u:A => Rstar_R x u y).  
   
-Theorem Rstar_Rstar':  (x:A)(y:A)(Rstar x y)->(Rstar' x y).
- Proof  [x:A][y:A][h:(Rstar x y)](h Rstar' ([u:A](Rstar'_reflexive u))
-         ([u:A][v:A][w:A][h1:(R u v)][h2:(Rstar' v w)]
-          (Rstar'_R u w v h1 (Rstar'_Rstar v w h2)))).  
+Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y.
+ Proof
+   fun (x y:A) (h:Rstar x y) =>
+     h Rstar' (fun u:A => Rstar'_reflexive u)
+       (fun (u v w:A) (h1:R u v) (h2:Rstar' v w) =>
+          Rstar'_R u w v h1 (Rstar'_Rstar v w h2)).  
 
 
 (** Property of Commutativity of two relations *)
 
-Definition commut := [A:Set][R1,R2:A->A->Prop]
-                       (x,y:A)(R1 y x)->(z:A)(R2 z y)
-                        ->(EX y':A |(R2 y' x) & (R1 z y')).
+Definition commut (A:Set) (R1 R2:A -> A -> Prop) :=
+  forall x y:A,
+    R1 y x -> forall z:A, R2 z y ->  exists2 y' : A | R2 y' x & R1 z y'.
 
 
 End Rstar.
-