Remplacement Euclid_def Euclid_proof par Euclid

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

11 files changed, 18 insertions, 28 deletions

diff --git a/Makefile b/Makefile
index 9b22c333d6..6e0d1dd2bc 100644
--- a/Makefile
+++ b/Makefile
@@ -347,8 +347,8 @@ ARITHVO=theories/Arith/Arith.vo         theories/Arith/Gt.vo          \
 	theories/Arith/Div2.vo          theories/Arith/Minus.vo       \
 	theories/Arith/Mult.vo          theories/Arith/Even.vo        \
 	theories/Arith/EqNat.vo         theories/Arith/Peano_dec.vo   \
-	theories/Arith/Euclid_def.vo    theories/Arith/Plus.vo        \
-	theories/Arith/Euclid_proof.vo  theories/Arith/Wf_nat.vo      \
+	theories/Arith/Euclid.vo        theories/Arith/Plus.vo        \
+	theories/Arith/Wf_nat.vo      \
 #	theories/Arith/Div.vo 
 
 BOOLVO=theories/Bool/Bool.vo  theories/Bool/IfProp.vo \
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 7917f15828..80c29c3951 100755
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Le.
 Require Export Lt.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 8513e6b52b..ab22eca22c 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Le.
 Require Lt.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index a439417558..172ccf568a 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (********************************************)
-(* equality is decidable on nat             *)
+(* Equality is decidable on [nat]           *)
 (********************************************)
 
 
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 72baafe3ac..1397326b24 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Le.
 Require Lt.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index 24f4ba36c7..959f501b94 100755
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Euclidean division *)
 
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 25b5d21da4..60fdc68ff6 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Lt.
 Require Plus.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index cd3e404cd8..8392f17cec 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (**************************************************************************)
 (*                    Equality on natural numbers                         *)
diff --git a/theories/Arith/Euclid_proof.v b/theories/Arith/Euclid.v
index e4034b0a5d..c6db2917bd 100755..100644
--- a/theories/Arith/Euclid_proof.v
+++ b/theories/Arith/Euclid.v
@@ -6,13 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
-Require Minus.
-Require Euclid_def.
+Require Mult.
 Require Compare_dec.
 Require Wf_nat.
 
+
+Inductive diveucl [a,b:nat] : Set 
+      := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b).
+
+
 Lemma eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b).
 Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
 Elim (le_gt_dec b n).
diff --git a/theories/Arith/Euclid_def.v b/theories/Arith/Euclid_def.v
deleted file mode 100755
index a30b93cafc..0000000000
--- a/theories/Arith/Euclid_def.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require Export Mult.
-
-Inductive diveucl [a,b:nat] : Set 
-      := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b).
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
index 7d922c5b6e..655de34ca8 100755
--- a/theories/Arith/intro.tex
+++ b/theories/Arith/intro.tex
@@ -46,7 +46,7 @@ properties of it.
 \item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows 
 the equivalence with Leibniz' equality.
 
-\item {\tt Euclid\_def.v} and {\tt Euclid\_prog.v} prove that the euclidean
+\item {\tt Euclid.v} proves that the euclidean
 division specification is realisable. Conversely, {\tt Div.v} exhibits
 two different algorithms and semi-automatically reconstruct the proof of
 their correctness. These files emphasize the extraction of program vs