deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf

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

4 files changed, 26 insertions, 23 deletions

diff --git a/.depend.coq b/.depend.coq
index 53788ead05..32a312384c 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -3,12 +3,11 @@ contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_ut
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
 contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
 contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
-contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
 contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo
 contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/ZArith/ZArith.vo theories/Bool/Sumbool.vo
 contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
 contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
-contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
+contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo theories/ZArith/Zwf.vo contrib/correctness/Arrays.vo
 contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
 contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
 contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
@@ -33,8 +32,13 @@ theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo the
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rgeom.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
 theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo
+theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
+theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
+theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Init/Specif.vo
+theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Init/Specif.vo
 theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo
 theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
@@ -111,6 +115,7 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
diff --git a/Makefile b/Makefile
index 15e2d236dc..84c8059581 100644
--- a/Makefile
+++ b/Makefile
@@ -455,7 +455,8 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/Zmisc.vo       theories/ZArith/zarith_aux.vo \
 	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
 	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
-	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo
+	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo \
+	 theories/ZArith/Zwf.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
@@ -558,8 +559,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo				\
 	contrib/correctness/Exchange.vo					\
 	contrib/correctness/ArrayPermut.vo				\
 	contrib/correctness/ProgBool.vo contrib/correctness/ProgInt.vo	\
-	contrib/correctness/ProgWf.vo contrib/correctness/Sorted.vo	\
-	contrib/correctness/Tuples.vo
+	contrib/correctness/Sorted.vo	contrib/correctness/Tuples.vo
 #	contrib/correctness/ProgramsExtraction.vo			
 
 OMEGAVO = contrib/omega/Omega.vo
diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index 5cc7b6aa74..8f3f90b95e 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -16,7 +16,7 @@ Require Export Tuples.
 
 Require Export ProgInt.
 Require Export ProgBool.
-Require Export ProgWf.
+Require Export Zwf.
 
 Require Export Arrays.
 
diff --git a/contrib/correctness/ProgWf.v b/theories/ZArith/Zwf.v
index f51506d21c..386317e831 100644
--- a/contrib/correctness/ProgWf.v
+++ b/theories/ZArith/Zwf.v
@@ -6,31 +6,29 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Certification of Imperative Programs / Jean-Christophe Filliātre *)
-
 (* $Id$ *)
 
 Require ZArith.
 Require Export Wf_nat.
 
-(* Well-founded relations on Z. *)
+(** Well-founded relations on Z. *)
+
+(** We define the following family of relations on [Z x Z]: 
 
-(* We define the following family of relations on ZxZ : 
- * 
- *      x (Zwf c) y   iff   c <= x < y
+    [x (Zwf c) y]   iff   [c <= x < y]
  *)
 
 Definition Zwf := [c:Z][x,y:Z] `c <= x` /\ `c <= y` /\ `x < y`.
 
 
-(* and we prove that (Zwf c) is well founded *)
+(** and we prove that [(Zwf c)] is well founded *)
 
 Section wf_proof.
 
 Variable c : Z.
 
-(* The proof of well-foundness is classic : we do the proof by induction
- * on a measure in nat, which is here |x-c| *)
+(** The proof of well-foundness is classic: we do the proof by induction
+    on a measure in nat, which is here [|x-c|] *)
 
 Local f := [z:Z](absolu (Zminus z c)).
 
@@ -51,21 +49,21 @@ End wf_proof.
 Hints Resolve Zwf_well_founded : datatypes v62.
 
 
-(* We also define the other family of relations :
- *
- *      x (Zwf_up c) y   iff   y < x <= c
+(** We also define the other family of relations:
+
+    [x (Zwf_up c) y]   iff   [y < x <= c]
  *)
 
 Definition Zwf_up := [c:Z][x,y:Z] `y < x <= c`.
 
-(* and we prove that (Zwf_up c) is well founded *)
+(** and we prove that [(Zwf_up c)] is well founded *)
 
 Section wf_proof_up.
 
 Variable c : Z.
 
-(* The proof of well-foundness is classic : we do the proof by induction
- * on a measure in nat, which is here |c-x| *)
+(** The proof of well-foundness is classic: we do the proof by induction
+    on a measure in nat, which is here [|c-x|] *)
 
 Local f := [z:Z](absolu (Zminus c z)).