suppression d'axiomes dans Rstar, Newman et Integers

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

2 files changed, 22 insertions, 2 deletions

diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index e7829b00e..2fe408543 100755
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -10,6 +10,16 @@
 
 Require Rstar.
 
+Section Newman.
+
+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).
+
 Definition coherence := [x:A][y:A] (exT2 ? (Rstar x) (Rstar y)).
 
 Theorem coherence_intro :  (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y).
@@ -99,3 +109,7 @@ Theorem Newman : (x:A)(confluence x).
 Proof [x:A](Hyp1 x confluence Ind_proof).  
 
 End Newman_section.
+
+
+End Newman.
+
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index a0aaed9ad..ff2e02a4b 100755
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -10,8 +10,10 @@
 
 (* Properties of a binary relation R on type A *)
 
-Parameter A : Type.  
-Parameter R : A->A->Prop.  
+Section Rstar.
+
+Variable A : Type.  
+Variable R : A->A->Prop.  
 
 (* Definition of the reflexive-transitive closure R* of R *)
 (* Smallest reflexive P containing R o P *)
@@ -71,3 +73,7 @@ Theorem Rstar_Rstar':  (x:A)(y:A)(Rstar x y)->(Rstar' x y).
 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')).
+
+
+End Rstar.
+