Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans le

répertoire Num. Suppression de ce dernier de l'archive courante.



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

36 files changed, 0 insertions, 1405 deletions

diff --git a/theories/Num/.depend b/theories/Num/.depend
deleted file mode 100644
index e231ff802..000000000
--- a/theories/Num/.depend
+++ /dev/null
@@ -1,72 +0,0 @@
-SubProps.vo: SubProps.v
-SubProps.vi: SubProps.v
-Params.vo: Params.v
-Params.vi: Params.v
-OppProps.vo: OppProps.v
-OppProps.vi: OppProps.v
-OppAxioms.vo: OppAxioms.v
-OppAxioms.vi: OppAxioms.v
-NeqProps.vo: NeqProps.v NeqParams.vo NeqAxioms.vo EqParams.vo EqAxioms.vo
-NeqProps.vi: NeqProps.v NeqParams.vo NeqAxioms.vo EqParams.vo EqAxioms.vo
-NeqParams.vo: NeqParams.v Params.vo
-NeqParams.vi: NeqParams.v Params.vo
-NeqDef.vo: NeqDef.v Params.vo EqParams.vo
-NeqDef.vi: NeqDef.v Params.vo EqParams.vo
-NeqAxioms.vo: NeqAxioms.v EqParams.vo NeqParams.vo
-NeqAxioms.vi: NeqAxioms.v EqParams.vo NeqParams.vo
-NatSyntax.vo: NatSyntax.v
-NatSyntax.vi: NatSyntax.v
-NSyntax.vo: NSyntax.v Params.vo
-NSyntax.vi: NSyntax.v Params.vo
-LtProps.vo: LtProps.v Axioms.vo AddProps.vo
-LtProps.vi: LtProps.v Axioms.vo AddProps.vo
-LeProps.vo: LeProps.v LtProps.vo LeAxioms.vo
-LeProps.vi: LeProps.v LtProps.vo LeAxioms.vo
-LeAxioms.vo: LeAxioms.v Axioms.vo LtProps.vo
-LeAxioms.vi: LeAxioms.v Axioms.vo LtProps.vo
-GtProps.vo: GtProps.v
-GtProps.vi: GtProps.v
-GtAxioms.vo: GtAxioms.v Axioms.vo LeProps.vo
-GtAxioms.vi: GtAxioms.v Axioms.vo LeProps.vo
-GeProps.vo: GeProps.v
-GeProps.vi: GeProps.v
-GeAxioms.vo: GeAxioms.v Axioms.vo LtProps.vo
-GeAxioms.vi: GeAxioms.v Axioms.vo LtProps.vo
-EqParams.vo: EqParams.v Params.vo
-EqParams.vi: EqParams.v Params.vo
-EqAxioms.vo: EqAxioms.v Params.vo EqParams.vo NSyntax.vo
-EqAxioms.vi: EqAxioms.v Params.vo EqParams.vo NSyntax.vo
-DiscrProps.vo: DiscrProps.v DiscrAxioms.vo LtProps.vo
-DiscrProps.vi: DiscrProps.v DiscrAxioms.vo LtProps.vo
-DiscrAxioms.vo: DiscrAxioms.v Params.vo NSyntax.vo
-DiscrAxioms.vi: DiscrAxioms.v Params.vo NSyntax.vo
-Definitions.vo: Definitions.v
-Definitions.vi: Definitions.v
-Axioms.vo: Axioms.v Params.vo EqParams.vo NSyntax.vo
-Axioms.vi: Axioms.v Params.vo EqParams.vo NSyntax.vo
-AddProps.vo: AddProps.v Axioms.vo EqAxioms.vo NeqProps.vo
-AddProps.vi: AddProps.v Axioms.vo EqAxioms.vo NeqProps.vo
-SubProps.html: SubProps.v
-Params.html: Params.v
-OppProps.html: OppProps.v
-OppAxioms.html: OppAxioms.v
-NeqProps.html: NeqProps.v NeqParams.html NeqAxioms.html EqParams.html EqAxioms.html
-NeqParams.html: NeqParams.v Params.html
-NeqDef.html: NeqDef.v Params.html EqParams.html
-NeqAxioms.html: NeqAxioms.v EqParams.html NeqParams.html
-NatSyntax.html: NatSyntax.v
-NSyntax.html: NSyntax.v Params.html
-LtProps.html: LtProps.v Axioms.html AddProps.html
-LeProps.html: LeProps.v LtProps.html LeAxioms.html
-LeAxioms.html: LeAxioms.v Axioms.html LtProps.html
-GtProps.html: GtProps.v
-GtAxioms.html: GtAxioms.v Axioms.html LeProps.html
-GeProps.html: GeProps.v
-GeAxioms.html: GeAxioms.v Axioms.html LtProps.html
-EqParams.html: EqParams.v Params.html
-EqAxioms.html: EqAxioms.v Params.html EqParams.html NSyntax.html
-DiscrProps.html: DiscrProps.v DiscrAxioms.html LtProps.html
-DiscrAxioms.html: DiscrAxioms.v Params.html NSyntax.html
-Definitions.html: Definitions.v
-Axioms.html: Axioms.v Params.html EqParams.html NSyntax.html
-AddProps.html: AddProps.v Axioms.html EqAxioms.html NeqProps.html
diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
deleted file mode 100644
index 7c291aff5..000000000
--- a/theories/Num/AddProps.v
+++ /dev/null
@@ -1,57 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Axioms.
-Require Export EqAxioms.
-
-(** This file contains basic properties of addition with respect to equality *)
-
-(** Properties of Addition *)
-Lemma add_x_0 : (x:N)(x+zero)=x.
-EAuto 3 with num.
-Qed.
-Hints Resolve add_x_0 : num.
-
-Lemma add_x_Sy : (x,y:N)(x+(S y))=(S (x+y)).
-Intros x y; Apply eq_trans with (S y)+x; EAuto with num.
-Qed.
-
-Hints Resolve add_x_Sy : num.
-
-Lemma add_x_Sy_swap : (x,y:N)(x+(S y))=((S x)+y).
-EAuto with num.
-Qed.
-Hints Resolve add_x_Sy_swap : num.
-
-Lemma add_Sx_y_swap : (x,y:N)((S x)+y)=(x+(S y)).
-Auto with num.
-Qed.
-Hints Resolve add_Sx_y_swap : num.
-
-
-Lemma add_assoc_r : (x,y,z:N)(x+(y+z))=((x+y)+z).
-Auto with num.
-Qed.
-Hints Resolve add_assoc_r : num.
-
-Lemma add_x_y_z_perm : (x,y,z:N)((x+y)+z)=(y+(x+z)).
-EAuto with num.
-Qed.
-Hints Resolve add_x_y_z_perm : num.
-
-Lemma add_x_one_S : (x:N)(x+one)=(S x).
-Intros; Apply eq_trans with (x+(S zero)); EAuto with num.
-Qed.
-Hints Resolve add_x_one_S : num.
-
-Lemma add_one_x_S : (x:N)(one+x)=(S x).
-Intros; Apply eq_trans with (x+one); Auto with num.
-Qed.
-Hints Resolve add_one_x_S : num.
-
-
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
deleted file mode 100644
index 5c945bdd4..000000000
--- a/theories/Num/Axioms.v
+++ /dev/null
@@ -1,46 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** Axioms for the basic numerical operations *)
-Require Export Params.
-Require Export EqParams.
-Require Export NSyntax.
-
-(** Axioms for [eq] *)
-
-Axiom eq_refl : (x:N)(x=x).
-Axiom eq_sym : (x,y:N)(x=y)->(y=x).
-Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
-
-(** Axioms for [add] *)
-
-Axiom add_sym : (x,y:N)(x+y)=(y+x).
-Axiom add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
-Axiom add_0_x : (x:N)(zero+x)=x.
-
-(** Axioms for [S] *)
-Axiom add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
-
-(** Axioms for [one] *)
-Axiom S_0_1 : (S zero)=one.
-
-(** Axioms for [<], 
-    properties of [>], [<=] and [>=] will be derived from [<] *)
-
-Axiom lt_trans : (x,y,z:N)x<y->y<z->x<z.
-Axiom lt_anti_refl : (x:N)~(x<x).
-
-Axiom lt_x_Sx : (x:N)x<(S x).
-Axiom lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
-
-Axiom lt_add_compat_l : (x,y,z:N)(x<y)->((x+z)<(y+z)).
-
-Hints Resolve add_sym add_assoc_l add_0_x add_Sx_y S_0_1 lt_x_Sx lt_S_compat
-              lt_trans lt_anti_refl lt_add_compat_l : num.
diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v
deleted file mode 100644
index 8ba3314b8..000000000
--- a/theories/Num/Definitions.v
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** Axiomatisation of a numerical set 
-
-  It will be instantiated by Z and R later on
-  We choose to introduce many operation to allow flexibility in definition 
-  ([S] is primitive in the definition of [nat] while [add] and [one] 
-   are primitive in the definition 
-*)
-
-Parameter N:Type.
-Parameter zero:N.
-Parameter one:N.
-Parameter add:N->N->N.
-Parameter S:N->N.
-
-(** Relations *)
-Parameter eq,lt,le,gt,ge:N->N->Prop.    
-Definition neq [x,y:N] := (eq x y)->False.
-
diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v
deleted file mode 100644
index c48dc7062..000000000
--- a/theories/Num/DiscrAxioms.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export Params.
-Require Export NSyntax.
-
-(** Axiom for a discrete set *)
-
-Axiom lt_x_Sy_le : (x,y:N)(x<(S y))->(x<=y).
-Hints Resolve lt_x_Sy_le : num.
diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v
deleted file mode 100644
index 70cf66681..000000000
--- a/theories/Num/DiscrProps.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export DiscrAxioms.
-Require Export LtProps.
-
-(** Properties of a discrete order *)
-
-Lemma lt_le_Sx_y : (x,y:N)(x<y) -> ((S x)<=y).
-EAuto with num.
-Qed.
-Hints Resolve lt_le_Sx_y : num.
\ No newline at end of file
diff --git a/theories/Num/EqAxioms.v b/theories/Num/EqAxioms.v
deleted file mode 100644
index 521c0cd97..000000000
--- a/theories/Num/EqAxioms.v
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** Axioms for equality *)
-Require Export Params.
-Require Export EqParams.
-Require Export NSyntax.
-
-(** Basic Axioms for [eq] *)
-
-Axiom eq_refl : (x:N)(x=x).
-Axiom eq_sym : (x,y:N)(x=y)->(y=x).
-Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
-
-(** Axioms for [eq] and [add] *)
-Axiom add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
-
-(** Axioms for [eq] and [S] *)
-Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
-
-(** Axioms for [eq] and [<] *)
-Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
-
-Hints Resolve eq_refl eq_trans add_eq_compat S_eq_compat lt_eq_compat : num.
-Hints Immediate eq_sym : num.
diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v
deleted file mode 100644
index 53a24c314..000000000
--- a/theories/Num/EqParams.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** Equality is introduced as an independant parameter, it could be 
-    instantiated with Leibniz equality *)
-Require Export Params.
-
-Parameter eqN:N->N->Prop.  
-
-(*i Infix 6 "=" eqN V8only 50. i*)
-
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-
-Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
-.
diff --git a/theories/Num/GeAxioms.v b/theories/Num/GeAxioms.v
deleted file mode 100644
index b618fca78..000000000
--- a/theories/Num/GeAxioms.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export Axioms.
-Require Export LtProps.
-
-(** Axiomatizing [>=] from [<] *)
-
-Axiom not_lt_ge : (x,y:N)~(x<y)->(x>=y).
-Axiom ge_not_lt : (x,y:N)(x>=y)->~(x<y).
-
-Hints Resolve not_lt_ge : num.
-Hints Immediate ge_not_lt : num.
diff --git a/theories/Num/GeProps.v b/theories/Num/GeProps.v
deleted file mode 100644
index 57945e47e..000000000
--- a/theories/Num/GeProps.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
diff --git a/theories/Num/GtAxioms.v b/theories/Num/GtAxioms.v
deleted file mode 100644
index 8f49a3412..000000000
--- a/theories/Num/GtAxioms.v
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export Axioms.
-Require Export LeProps.
-
-(** Axiomatizing [>] from [<] *)
-
-Axiom not_le_gt : (x,y:N)~(x<=y)->(x>y).
-Axiom gt_not_le : (x,y:N)(x>y)->~(x<=y).
-
-Hints Resolve not_le_gt : num.
-
-Hints Immediate gt_not_le : num.
diff --git a/theories/Num/GtProps.v b/theories/Num/GtProps.v
deleted file mode 100644
index 57945e47e..000000000
--- a/theories/Num/GtProps.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
diff --git a/theories/Num/LeAxioms.v b/theories/Num/LeAxioms.v
deleted file mode 100644
index fcb04572b..000000000
--- a/theories/Num/LeAxioms.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Export Axioms.
-Require Export LtProps.
-
-(** Axiomatizing [<=] from [<] *)
-
-Axiom lt_or_eq_le : (x,y:N)((x<y)\/(x=y))->(x<=y).
-Axiom le_lt_or_eq : (x,y:N)(x<=y)->(x<y)\/(x=y).
-
-Hints Resolve lt_or_eq_le : num.
-Hints Immediate le_lt_or_eq : num.
diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v
deleted file mode 100644
index e34d23122..000000000
--- a/theories/Num/LeProps.v
+++ /dev/null
@@ -1,104 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export LtProps.
-Require Export LeAxioms.
-
-(** Properties of the relation [<=] *)
-
-Lemma lt_le : (x,y:N)(x<y)->(x<=y).
-Auto with num.
-Qed.
-
-Lemma eq_le : (x,y:N)(x=y)->(x<=y).
-Auto with num.
-Qed.
-
-(** compatibility with equality *)
-Lemma le_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<=x2)->(y1<=y2).
-Intros x1 x2 y1 y2 eq1 eq2 le1; Case le_lt_or_eq with 1:=le1; Intro.
-EAuto with num.
-Apply eq_le; Apply eq_trans with x1; EAuto with num.
-Qed.
-Hints Resolve le_eq_compat : num.
-
-(** Transitivity *)
-Lemma le_trans : (x,y,z:N)(x<=y)->(y<=z)->(x<=z).
-Intros x y z le1 le2.
-Case le_lt_or_eq with 1:=le1; Intro.
-Case le_lt_or_eq with 1:=le2; EAuto with num.
-EAuto with num.
-Qed.
-Hints Resolve le_trans : num.
-
-(** compatibility with equality, addition and successor *)
-Lemma le_add_compat_l : (x,y,z:N)(x<=y)->((x+z)<=(y+z)).
-Intros x y z le1.
-Case le_lt_or_eq with 1:=le1; EAuto with num.
-Qed.
-Hints Resolve le_add_compat_l : num.
-
-Lemma le_add_compat_r : (x,y,z:N)(x<=y)->((z+x)<=(z+y)).
-Intros x y z H; Apply le_eq_compat with (x+z) (y+z); Auto with num.
-Qed.
-Hints Resolve le_add_compat_r : num.
-
-Lemma le_add_compat : (x1,x2,y1,y2:N)(x1<=x2)->(y1<=y2)->((x1+y1)<=(x2+y2)).
-Intros; Apply le_trans with (x1+y2); Auto with num.
-Qed.
-Hints Immediate le_add_compat : num.
-
-(* compatibility with successor *)
-Lemma le_S_compat : (x,y:N)(x<=y)->((S x)<=(S y)).
-Intros x y le1.
-Case le_lt_or_eq with 1:=le1; EAuto with num.
-Qed.
-Hints Resolve le_S_compat : num.
-
-
-(** relating [<=] with [<] *)
-Lemma le_lt_x_Sy : (x,y:N)(x<=y)->(x<(S y)).
-Intros x y le1.
-Case le_lt_or_eq with 1:=le1; Auto with num.
-Qed.
-Hints Immediate le_lt_x_Sy : num.
-
-Lemma le_le_x_Sy : (x,y:N)(x<=y)->(x<=(S y)).
-Auto with num.
-Qed.
-Hints Immediate le_le_x_Sy : num.
-
-Lemma le_Sx_y_lt : (x,y:N)((S x)<=y)->(x<y).
-Intros x y le1.
-Case le_lt_or_eq with 1:=le1; EAuto with num.
-Qed.
-Hints Immediate le_Sx_y_lt : num.
-
-(** Combined transitivity *)
-Lemma lt_le_trans : (x,y,z:N)(x<y)->(y<=z)->(x<z).
-Intros x y z lt1 le1; Case le_lt_or_eq with 1:= le1; EAuto with num.
-Qed.
-
-Lemma le_lt_trans : (x,y,z:N)(x<=y)->(y<z)->(x<z).
-Intros x y z le1 lt1; Case le_lt_or_eq with 1:= le1; EAuto with num.
-Qed.
-Hints Immediate lt_le_trans le_lt_trans : num.
-
-(** weaker compatibility results involving [<] and [<=] *)
-Lemma lt_add_compat_weak_l : (x1,x2,y1,y2:N)(x1<=x2)->(y1<y2)->((x1+y1)<(x2+y2)).
-Intros; Apply lt_le_trans with (x1+y2); Auto with num.
-Qed.
-Hints Immediate  lt_add_compat_weak_l : num.
-
-Lemma lt_add_compat_weak_r : (x1,x2,y1,y2:N)(x1<x2)->(y1<=y2)->((x1+y1)<(x2+y2)).
-Intros; Apply le_lt_trans with (x1+y2); Auto with num.
-Qed.
-Hints Immediate lt_add_compat_weak_r : num.
-
-
-
diff --git a/theories/Num/Leibniz/.depend b/theories/Num/Leibniz/.depend
deleted file mode 100644
index b6ddc78aa..000000000
--- a/theories/Num/Leibniz/.depend
+++ /dev/null
@@ -1,9 +0,0 @@
-Params.vo: Params.v
-Params.vi: Params.v
-NSyntax.vo: NSyntax.v Params.vo
-NSyntax.vi: NSyntax.v Params.vo
-EqAxioms.vo: EqAxioms.v NSyntax.vo
-EqAxioms.vi: EqAxioms.v NSyntax.vo
-Params.html: Params.v
-NSyntax.html: NSyntax.v Params.html
-EqAxioms.html: EqAxioms.v NSyntax.html
diff --git a/theories/Num/Leibniz/EqAxioms.v b/theories/Num/Leibniz/EqAxioms.v
deleted file mode 100644
index 46d835eeb..000000000
--- a/theories/Num/Leibniz/EqAxioms.v
+++ /dev/null
@@ -1,50 +0,0 @@
-
-(*s Instantiating [eqN] with Leibniz equality *)
-
-Require NSyntax.
-
-Definition eqN [x,y:N] := (x==y).
-Hints Unfold eqN : num.
-
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-
-Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ].
-
-(*s Lemmas for [eqN] *)
-
-Lemma eq_refl : (x:N)(x=x).
-Auto with num.
-Save.
-
-Lemma eq_sym : (x,y:N)(x=y)->(y=x).
-Unfold eqN; Auto.
-Save.
-
-Lemma eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
-Intros; Red; Transitivity y; Auto.
-Save.
-
-Hints Resolve eq_refl eq_trans : num.
-Hints Immediate eq_sym : num.
-
-(*s Compatibility lemmas for [S], [add], [lt] *)
-Lemma S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
-Intros x y eq1; Unfold eqN; Rewrite eq1; Auto.
-Save.
-Hints Resolve S_eq_compat : nat.
-
-Lemma add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
-Intros x1 x2 y1 y2 eq1 eq2;Unfold eqN;  Rewrite eq1; Rewrite eq2; Auto.
-Save.
-Hints Resolve add_eq_compat : nat.
-
-Lemma lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
-Intros x1 x2 y1 y2 eq1 eq2; Unfold eqN; Rewrite eq1; Rewrite eq2; Trivial.
-Save.
-
-Hints Resolve add_eq_compat S_eq_compat lt_eq_compat : num.
-
- 
\ No newline at end of file
diff --git a/theories/Num/Leibniz/Make b/theories/Num/Leibniz/Make
deleted file mode 100644
index 0b35afabb..000000000
--- a/theories/Num/Leibniz/Make
+++ /dev/null
@@ -1,3 +0,0 @@
-EqAxioms.v 
-NSyntax.v 
-Params.v 
diff --git a/theories/Num/Leibniz/NSyntax.v b/theories/Num/Leibniz/NSyntax.v
deleted file mode 100644
index 62613512b..000000000
--- a/theories/Num/Leibniz/NSyntax.v
+++ /dev/null
@@ -1,32 +0,0 @@
-
-(*s Syntax for arithmetic *)
-
-Require Export Params.
-
-Infix 6 "<" lt.
-Infix 6 "<=" le.
-Infix 6 ">" gt.
-Infix 6 ">=" ge.
-
-(*i Infix 7 "+" plus. i*)
-
-Grammar constr lassoc_constr4 :=
-  squash_sum
-  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
-      case [$c2] of
-        (SQUASH $T2) ->
-            case [$c1] of
-              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
-            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
-            esac
-      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
-      esac.
-
-Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
- ;
-
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
\ No newline at end of file
diff --git a/theories/Num/Leibniz/Params.v b/theories/Num/Leibniz/Params.v
deleted file mode 100644
index c8cb772de..000000000
--- a/theories/Num/Leibniz/Params.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(*i $Id$ i*)
-
-(*s 
-  Axiomatisation of a numerical set 
-  It will be instantiated by Z and R later on
-  We choose to introduce many operation to allow flexibility in definition 
-  ([S] is primitive in the definition of [nat] while [add] and [one] 
-   are primitive in the definition 
-*)
-
-Parameter N:Type.
-Parameter zero:N.
-Parameter one:N.
-Parameter add:N->N->N.
-Parameter S:N->N.
-
-(*s Relations, equality is defined separately *)
-Parameter lt,le,gt,ge:N->N->Prop.    
-
-
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
deleted file mode 100644
index 79f0f3303..000000000
--- a/theories/Num/LtProps.v
+++ /dev/null
@@ -1,82 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Axioms.
-Require Export AddProps.
-Require Export NeqProps.
-
-(** This file contains basic properties of the less than relation *)
-
-
-Lemma lt_anti_sym : (x,y:N)x<y->~(y<x).
-Red; Intros x y lt1 lt2; Apply (lt_anti_refl x); EAuto with num.
-Qed.
-Hints Resolve lt_anti_refl : num.
-
-Lemma eq_not_lt : (x,y:N)(x=y)->~(x<y).
-Red; Intros x y eq1 lt1; Apply (lt_anti_refl x); EAuto with num.
-Qed.
-Hints Resolve eq_not_lt : num.
-
-Lemma lt_0_1 : (zero<one).
-EAuto with num.
-Qed.
-Hints Resolve lt_0_1 : num.
-
-
-Lemma eq_lt_x_Sy : (x,y:N)(x=y)->(x<(S y)).
-EAuto with num.
-Qed.
-Hints Resolve eq_lt_x_Sy : num.
-
-Lemma lt_lt_x_Sy : (x,y:N)(x<y)->(x<(S y)).
-EAuto with num.
-Qed.
-Hints Immediate lt_lt_x_Sy : num.
-
-Lemma lt_Sx_y_lt : (x,y:N)((S x)<y)->(x<y).
-EAuto with num.
-Qed.
-Hints Immediate lt_Sx_y_lt : num.
-
-(** Relating [<] and [=] *)
-
-Lemma lt_neq : (x,y:N)(x<y)->(x<>y).
-Red; Intros x y lt1 eq1; Apply (lt_anti_refl x); EAuto with num.
-Qed.
-Hints Immediate lt_neq : num.
-
-Lemma lt_neq_sym : (x,y:N)(y<x)->(x<>y).
-Intros x y lt1 ; Apply neq_sym; Auto with num.
-Qed.
-Hints Immediate lt_neq_sym : num.
-
-(** Application to inequalities properties *)
-
-Lemma neq_x_Sx : (x:N)x<>(S x).
-Auto with num.
-Qed.
-Hints Resolve neq_x_Sx : num.
-
-Lemma neq_0_1 : zero<>one.
-Auto with num.
-Qed.
-Hints Resolve neq_0_1 : num.
-
-(** Relating [<] and [+] *)
-
-Lemma lt_add_compat_r : (x,y,z:N)(x<y)->((z+x)<(z+y)).
-Intros x y z H; Apply lt_eq_compat with (x+z) (y+z); Auto with num.
-Qed.
-Hints Resolve lt_add_compat_r : num.
-
-Lemma lt_add_compat : (x1,x2,y1,y2:N)(x1<x2)->(y1<y2)->((x1+y1)<(x2+y2)).
-Intros; Apply lt_trans with (x1+y2); Auto with num.
-Qed.
-Hints Immediate lt_add_compat : num.
-
diff --git a/theories/Num/Make b/theories/Num/Make
deleted file mode 100644
index c7c0595c7..000000000
--- a/theories/Num/Make
+++ /dev/null
@@ -1,26 +0,0 @@
-Params.v
-EqParams.v
-NSyntax.v
-
-Axioms.v
-EqAxioms.v
-
-NeqParams.v
-NeqAxioms.v
-NeqDef.v
-NeqProps.v
-AddProps.v
-LtProps.v
-OppProps.v
-SubProps.v
-LeAxioms.v
-LeProps.v
-GtAxioms.v
-GtProps.v
-GeAxioms.v
-GeProps.v
-DiscrAxioms.v
-DiscrProps.v
-OppAxioms.v
-Leibniz
-Nat
diff --git a/theories/Num/Makefile b/theories/Num/Makefile
deleted file mode 100644
index fdbe44bb6..000000000
--- a/theories/Num/Makefile
+++ /dev/null
@@ -1,343 +0,0 @@
-##############################################################################
-##                 The Calculus of Inductive Constructions                  ##
-##                                                                          ##
-##                                Projet Coq                                ##
-##                                                                          ##
-##                     INRIA                        ENS-CNRS                ##
-##              Rocquencourt                        Lyon                    ##
-##                                                                          ##
-##                                  Coq V7                                  ##
-##                                                                          ##
-##                                                                          ##
-##############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated by coq_makefile
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile 
-#
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-CAMLP4LIB=`camlp4 -where`
-COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
-  -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
-  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
-  -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
-ZFLAGS=$(OCAMLLIBS) $(COQSRC)
-OPT=
-COQFLAGS=-q $(OPT) $(COQLIBS)
-COQC=$(COQBIN)coqc
-GALLINA=gallina
-COQ2HTML=coq2html
-COQ2LATEX=coq2latex
-CAMLC=ocamlc -c
-CAMLOPTC=ocamlopt -c
-CAMLLINK=ocamlc
-CAMLOPTLINK=ocamlopt
-COQDEP=$(COQBIN)coqdep -c
-COQVO2XML=coq_vo2xml
-
-#########################
-#                       #
-# Libraries definition. #
-#                       #
-#########################
-
-OCAMLLIBS=-I .
-COQLIBS=-I .
-
-###################################
-#                                 #
-# Definition of the "all" target. #
-#                                 #
-###################################
-
-all: Params.vo\
-  EqParams.vo\
-  NSyntax.vo\
-  Axioms.vo\
-  EqAxioms.vo\
-  NeqParams.vo\
-  NeqAxioms.vo\
-  NeqDef.vo\
-  NeqProps.vo\
-  AddProps.vo\
-  LtProps.vo\
-  OppProps.vo\
-  SubProps.vo\
-  LeAxioms.vo\
-  LeProps.vo\
-  GtAxioms.vo\
-  GtProps.vo\
-  GeAxioms.vo\
-  GeProps.vo\
-  DiscrAxioms.vo\
-  DiscrProps.vo\
-  OppAxioms.vo\
-  Leibniz\
-  Nat
-
-spec: Params.vi\
-  EqParams.vi\
-  NSyntax.vi\
-  Axioms.vi\
-  EqAxioms.vi\
-  NeqParams.vi\
-  NeqAxioms.vi\
-  NeqDef.vi\
-  NeqProps.vi\
-  AddProps.vi\
-  LtProps.vi\
-  OppProps.vi\
-  SubProps.vi\
-  LeAxioms.vi\
-  LeProps.vi\
-  GtAxioms.vi\
-  GtProps.vi\
-  GeAxioms.vi\
-  GeProps.vi\
-  DiscrAxioms.vi\
-  DiscrProps.vi\
-  OppAxioms.vi
-
-gallina: Params.g\
-  EqParams.g\
-  NSyntax.g\
-  Axioms.g\
-  EqAxioms.g\
-  NeqParams.g\
-  NeqAxioms.g\
-  NeqDef.g\
-  NeqProps.g\
-  AddProps.g\
-  LtProps.g\
-  OppProps.g\
-  SubProps.g\
-  LeAxioms.g\
-  LeProps.g\
-  GtAxioms.g\
-  GtProps.g\
-  GeAxioms.g\
-  GeProps.g\
-  DiscrAxioms.g\
-  DiscrProps.g\
-  OppAxioms.g
-
-html: Params.html\
-  EqParams.html\
-  NSyntax.html\
-  Axioms.html\
-  EqAxioms.html\
-  NeqParams.html\
-  NeqAxioms.html\
-  NeqDef.html\
-  NeqProps.html\
-  AddProps.html\
-  LtProps.html\
-  OppProps.html\
-  SubProps.html\
-  LeAxioms.html\
-  LeProps.html\
-  GtAxioms.html\
-  GtProps.html\
-  GeAxioms.html\
-  GeProps.html\
-  DiscrAxioms.html\
-  DiscrProps.html\
-  OppAxioms.html
-
-tex: Params.tex\
-  EqParams.tex\
-  NSyntax.tex\
-  Axioms.tex\
-  EqAxioms.tex\
-  NeqParams.tex\
-  NeqAxioms.tex\
-  NeqDef.tex\
-  NeqProps.tex\
-  AddProps.tex\
-  LtProps.tex\
-  OppProps.tex\
-  SubProps.tex\
-  LeAxioms.tex\
-  LeProps.tex\
-  GtAxioms.tex\
-  GtProps.tex\
-  GeAxioms.tex\
-  GeProps.tex\
-  DiscrAxioms.tex\
-  DiscrProps.tex\
-  OppAxioms.tex
-
-gallinatex: Params.g.tex\
-  EqParams.g.tex\
-  NSyntax.g.tex\
-  Axioms.g.tex\
-  EqAxioms.g.tex\
-  NeqParams.g.tex\
-  NeqAxioms.g.tex\
-  NeqDef.g.tex\
-  NeqProps.g.tex\
-  AddProps.g.tex\
-  LtProps.g.tex\
-  OppProps.g.tex\
-  SubProps.g.tex\
-  LeAxioms.g.tex\
-  LeProps.g.tex\
-  GtAxioms.g.tex\
-  GtProps.g.tex\
-  GeAxioms.g.tex\
-  GeProps.g.tex\
-  DiscrAxioms.g.tex\
-  DiscrProps.g.tex\
-  OppAxioms.g.tex
-
-gallinahtml: Params.g.html\
-  EqParams.g.html\
-  NSyntax.g.html\
-  Axioms.g.html\
-  EqAxioms.g.html\
-  NeqParams.g.html\
-  NeqAxioms.g.html\
-  NeqDef.g.html\
-  NeqProps.g.html\
-  AddProps.g.html\
-  LtProps.g.html\
-  OppProps.g.html\
-  SubProps.g.html\
-  LeAxioms.g.html\
-  LeProps.g.html\
-  GtAxioms.g.html\
-  GtProps.g.html\
-  GeAxioms.g.html\
-  GeProps.g.html\
-  DiscrAxioms.g.html\
-  DiscrProps.g.html\
-  OppAxioms.g.html
-
-xml:: .xml_time_stamp
-.xml_time_stamp: Params.vo\
-  EqParams.vo\
-  NSyntax.vo\
-  Axioms.vo\
-  EqAxioms.vo\
-  NeqParams.vo\
-  NeqAxioms.vo\
-  NeqDef.vo\
-  NeqProps.vo\
-  AddProps.vo\
-  LtProps.vo\
-  OppProps.vo\
-  SubProps.vo\
-  LeAxioms.vo\
-  LeProps.vo\
-  GtAxioms.vo\
-  GtProps.vo\
-  GeAxioms.vo\
-  GeProps.vo\
-  DiscrAxioms.vo\
-  DiscrProps.vo\
-  OppAxioms.vo
-	$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
-	touch .xml_time_stamp
-
-###################
-#                 #
-# Subdirectories. #
-#                 #
-###################
-
-Leibniz:
-	cd Leibniz ; $(MAKE) all
-
-Nat:
-	cd Nat ; $(MAKE) all
-
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
-
-.PHONY: all opt byte archclean clean install depend xml Leibniz Nat
-
-.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
-
-.v.vo:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-.v.vi:
-	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-.v.g:
-	$(GALLINA) $<
-
-.v.html:
-	$(COQ2HTML) $<
-
-.v.tex:
-	$(COQ2LATEX) $< -latex -o $@
-
-.v.g.html:
-	$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@
-
-.v.g.tex:
-	$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@
-
-byte:
-	$(MAKE) all "OPT="
-
-opt:
-	$(MAKE) all "OPT=-opt"
-
-include .depend
-
-depend:
-	rm .depend
-	$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
-	$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
-	(cd Leibniz ; $(MAKE) depend)
-	(cd Nat ; $(MAKE) depend)
-
-xml::
-	(cd Leibniz ; $(MAKE) xml)
-	(cd Nat ; $(MAKE) xml)
-
-install:
-	@if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi
-	cp -f *.vo $(TARGETDIR)
-	(cd Leibniz ; $(MAKE) install)
-	(cd Nat ; $(MAKE) install)
-
-Makefile: Make
-	mv -f Makefile Makefile.bak
-	$(COQBIN)coq_makefile -f Make -o Makefile
-
-clean:
-	rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
-	(cd Leibniz ; $(MAKE) clean)
-	(cd Nat ; $(MAKE) clean)
-
-archclean:
-	rm -f *.cmx *.o
-	(cd Leibniz ; $(MAKE) archclean)
-	(cd Nat ; $(MAKE) archclean)
-
-# WARNING
-#
-# This Makefile has been automagically generated by coq_makefile
-# Edit at your own risks !
-#
-# END OF WARNING
-
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
deleted file mode 100644
index f32a3fa0c..000000000
--- a/theories/Num/NSyntax.v
+++ /dev/null
@@ -1,35 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Syntax for arithmetic *)
-
-Require Export Params.
-
-Infix 6 "<" lt V8only 70.
-Infix 6 "<=" le V8only 70.
-Infix 6 ">" gt V8only 70.
-Infix 6 ">=" ge V8only 70.
-
-(*i Infix 7 "+" plus V8only 50. i*)
-
-Grammar constr lassoc_constr4 :=
-  squash_sum
-  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
-      case [$c2] of
-        (SQUASH $T2) ->
-            case [$c1] of
-              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
-            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
-            esac
-      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
-      esac.
-
-Syntax constr
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
diff --git a/theories/Num/Nat/.depend b/theories/Num/Nat/.depend
deleted file mode 100644
index 8bfdf1fe5..000000000
--- a/theories/Num/Nat/.depend
+++ /dev/null
@@ -1,15 +0,0 @@
-Params.vo: Params.v
-Params.vi: Params.v
-NeqDef.vo: NeqDef.v Params.vo
-NeqDef.vi: NeqDef.v Params.vo
-NSyntax.vo: NSyntax.v
-NSyntax.vi: NSyntax.v
-EqAxioms.vo: EqAxioms.v NSyntax.vo
-EqAxioms.vi: EqAxioms.v NSyntax.vo
-Axioms.vo: Axioms.v Params.vo EqAxioms.vo NSyntax.vo
-Axioms.vi: Axioms.v Params.vo EqAxioms.vo NSyntax.vo
-Params.html: Params.v
-NeqDef.html: NeqDef.v Params.html
-NSyntax.html: NSyntax.v
-EqAxioms.html: EqAxioms.v NSyntax.html
-Axioms.html: Axioms.v Params.html EqAxioms.html NSyntax.html
diff --git a/theories/Num/Nat/Axioms.v b/theories/Num/Nat/Axioms.v
deleted file mode 100644
index 8d7333ac0..000000000
--- a/theories/Num/Nat/Axioms.v
+++ /dev/null
@@ -1,83 +0,0 @@
-(*i $Id$ i*)
-
-(*s Axioms for the basic numerical operations *)
-Require Export Params.
-Require Export EqAxioms.
-Require NSyntax.
-
-(*s Lemmas for [add] *)
-
-Lemma add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
-Induction y; Simpl; Auto with nat.
-Save.
-Hints Resolve add_Sx_y : nat.
-
-(*s Lemmas for [add] *)
-
-Lemma add_0_x : (x:N)(zero+x)=x.
-Induction x; Simpl; Auto with nat.
-Save.
-Hints Resolve add_0_x : nat.
-
-Lemma add_sym : (x,y:N)(x+y)=(y+x).
-Intros x y; Elim y; Simpl; Intros; Auto with nat.
-Rewrite H; Elim x; Simpl; Intros; Auto with nat.
-Save.
-Hints Resolve add_sym : nat.
-
-Lemma add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
-Intros x1 x2 y1 y2 eq1 eq2; Rewrite eq1; Rewrite eq2; Auto.
-Save.
-Hints Resolve add_eq_compat : nat.
-
-Lemma add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
-Intros x y z; Elim z; Simpl; Intros; Auto with nat.
-Save.
-
-
-
-(*s Lemmas for [one] *)
-Lemma S_0_1 : (S zero)=one.
-Auto.
-Save.
-
-(*s Lemmas for [<], 
-    properties of [>], [<=] and [>=] will be derived from [<] *)
-
-Lemma lt_trans : (x,y,z:N)x<y->y<z->x<z.
-Intros x y z lt1 lt2; Elim lt2; Unfold lt; Auto with nat.
-Save.
-Hints Resolve lt_trans : nat.
-
-Lemma lt_x_Sx : (x:N)x<(S x).
-Unfold lt; Auto with nat.
-Save.
-Hints Resolve lt_x_Sx : nat.
-
-Lemma lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
-Intros x y lt1; Elim lt1; Unfold lt; Auto with nat.
-Save.
-Hints Resolve lt_S_compat : nat.
-
-Lemma lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
-Intros x1 x2 y1 y2 eq1 eq2; Rewrite eq1; Rewrite eq2; Trivial.
-Save.
-
-Lemma lt_add_compat_l : (x,y,z:N)(x<y)->((x+z)<(y+z)).
-Intros x y z lt1; Elim z; Simpl; Auto with nat.
-Save.
-
-Lemma lt_Sx_Sy_lt : (x,y:N)((S x)<(S y))->(x<y).
-Intros x y lt1; Inversion lt1; EAuto with nat.
-Save.
-Hints Immediate lt_Sx_Sy_lt : nat.
-
-Lemma lt_anti_refl : (x:N)~(x<x).
-Induction x; Red; Intros.
-Inversion H.
-Auto with nat.
-Save.
-
-
-
-  
\ No newline at end of file
diff --git a/theories/Num/Nat/Make b/theories/Num/Nat/Make
deleted file mode 100644
index 4e81efed5..000000000
--- a/theories/Num/Nat/Make
+++ /dev/null
@@ -1,5 +0,0 @@
-Params.v
-EqAxioms.v
-Axioms.v
-NSyntax.v
-NeqDef.v
\ No newline at end of file
diff --git a/theories/Num/Nat/NSyntax.v b/theories/Num/Nat/NSyntax.v
deleted file mode 100644
index 9752dd2e9..000000000
--- a/theories/Num/Nat/NSyntax.v
+++ /dev/null
@@ -1,26 +0,0 @@
-
-(*s Syntax for arithmetic *)
-
-Infix 6 "<" lt.
-Infix 6 "<=" le.
-Infix 6 ">" gt.
-Infix 6 ">=" ge.
-
-(*i Infix 7 "+" plus. i*)
-
-Grammar constr lassoc_constr4 :=
-  squash_sum
-  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
-      case [$c2] of
-        (SQUASH $T2) ->
-            case [$c1] of
-              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
-            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
-            esac
-      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
-      esac.
-
-Syntax constr
-  level 4:
-    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
\ No newline at end of file
diff --git a/theories/Num/Nat/NeqDef.v b/theories/Num/Nat/NeqDef.v
deleted file mode 100644
index 8ce7df03a..000000000
--- a/theories/Num/Nat/NeqDef.v
+++ /dev/null
@@ -1,5 +0,0 @@
-
-(*s Definition of inequality *)
-
-Require Params.
-Definition neq [x,y:N] := (eqN x y)->False.
\ No newline at end of file
diff --git a/theories/Num/NeqAxioms.v b/theories/Num/NeqAxioms.v
deleted file mode 100644
index 8de6ade42..000000000
--- a/theories/Num/NeqAxioms.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** InEquality is introduced as an independant parameter, it could be 
-    instantiated with the negation of equality *)
-
-Require Export EqParams.
-Require Export NeqParams.
-
-Axiom eq_not_neq : (x,y:N)x=y->~(x<>y).
-Hints Immediate eq_not_neq : num.
-
-Axiom neq_sym : (x,y:N)(x<>y)->(y<>x).
-Hints Resolve neq_sym : num.
-
-Axiom neq_not_neq_trans : (x,y,z:N)(x<>y)->~(y<>z)->(x<>z).
-Hints Resolve neq_not_neq_trans : num.
-
-
-
-
-
-
-
-
-
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
deleted file mode 100644
index c7e8dcfd5..000000000
--- a/theories/Num/NeqDef.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** DisEquality is defined as the negation of equality *)
-
-Require Params.
-Require EqParams.
-Require EqAxioms.
-
-Definition neq : N -> N -> Prop := [x,y] ~(x=y).
-Infix 6 "<>" neq V8only 70.
-
-(* Proofs of axioms *)
-Lemma eq_not_neq : (x,y:N)x=y->~(x<>y).
-Unfold neq; Auto with num.
-Qed.
-Hints Immediate eq_not_neq : num.
-
-Lemma neq_sym : (x,y:N)(x<>y)->(y<>x).
-Unfold neq; Auto with num.
-Qed.
-Hints Resolve neq_sym : num.
-
-Lemma neq_not_neq_trans : (x,y,z:N)(x<>y)->~(y<>z)->(x<>z).
-Unfold neq; EAuto with num.
-Qed.
-Hints Resolve neq_not_neq_trans : num.
-
-
-
-
diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v
deleted file mode 100644
index 4fb2ca5aa..000000000
--- a/theories/Num/NeqParams.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** InEquality is introduced as an independant parameter, it could be 
-    instantiated with the negation of equality *)
-
-Require Export Params.
-
-Parameter neq : N -> N -> Prop.
-
-Infix 6 "<>" neq V8only 70.
-
-
-
-
-
-
-
diff --git a/theories/Num/NeqProps.v b/theories/Num/NeqProps.v
deleted file mode 100644
index d1da05c90..000000000
--- a/theories/Num/NeqProps.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export NeqParams.
-Require Export NeqAxioms.
-Require Export EqParams.
-Require Export EqAxioms.
-
-
-(** This file contains basic properties of disequality *)
-
-Lemma neq_antirefl : (x:N)~(x<>x).
-Auto with num.
-Qed.
-Hints Resolve neq_antirefl : num.
-
-Lemma eq_not_neq_y_x : (x,y:N)(x=y)->~(y<>x).
-Intros; Apply eq_not_neq; Auto with num.
-Qed.
-Hints Immediate eq_not_neq_y_x : num.
-
-Lemma neq_not_eq : (x,y:N)(x<>y)->~(x=y).
-Red; Intros; Apply (eq_not_neq x y); Trivial.
-Qed.
-Hints Immediate neq_not_eq : num.
-
-Lemma neq_not_eq_y_x : (x,y:N)(x<>y)->~(y=x).
-Intros; Apply neq_not_eq; Auto with num.
-Qed.
-Hints Immediate neq_not_eq_y_x : num.
-
-Lemma not_neq_neq_trans : (x,y,z:N)~(x<>y)->(y<>z)->(x<>z).
-Intros; Apply neq_sym; Apply neq_not_neq_trans with y; Auto with num.
-Qed.
-Hints Resolve not_neq_neq_trans : num.
-
-Lemma neq_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<>x2)->(y1<>y2).
-Intros.
-EAuto with num.
-Qed.
-
-
-
-
-
diff --git a/theories/Num/OppAxioms.v b/theories/Num/OppAxioms.v
deleted file mode 100644
index 57945e47e..000000000
--- a/theories/Num/OppAxioms.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
diff --git a/theories/Num/OppProps.v b/theories/Num/OppProps.v
deleted file mode 100644
index 57945e47e..000000000
--- a/theories/Num/OppProps.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
diff --git a/theories/Num/Params.v b/theories/Num/Params.v
deleted file mode 100644
index 394c016a3..000000000
--- a/theories/Num/Params.v
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(** 
-  Axiomatisation of a numerical set 
-
-  It will be instantiated by Z and R later on
-  We choose to introduce many operation to allow flexibility in definition 
-  ([S] is primitive in the definition of [nat] while [add] and [one] 
-   are primitive in the definition 
-*)
-
-Parameter N:Type.
-Parameter zero:N.
-Parameter one:N.
-Parameter add:N->N->N.
-Parameter S:N->N.
-
-(** Relations, equality is defined separately *)
-Parameter lt,le,gt,ge:N->N->Prop.    
-
-
diff --git a/theories/Num/SubProps.v b/theories/Num/SubProps.v
deleted file mode 100644
index 57945e47e..000000000
--- a/theories/Num/SubProps.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)