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

10 files changed, 16 insertions, 26 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 7917f1582..80c29c395 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 8513e6b52..ab22eca22 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 a43941755..172ccf568 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 72baafe3a..1397326b2 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 24f4ba36c..959f501b9 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 25b5d21da..60fdc68ff 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 cd3e404cd..8392f17ce 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 e4034b0a5..c6db2917b 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 a30b93caf..000000000
--- 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 7d922c5b6..655de34ca 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