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

5 files changed, 0 insertions, 134 deletions

diff --git a/theories/Num/Nat/.depend b/theories/Num/Nat/.depend
deleted file mode 100644
index 8bfdf1fe5f..0000000000
--- 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 8d7333ac09..0000000000
--- 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 4e81efed5b..0000000000
--- 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 9752dd2e9b..0000000000
--- 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 8ce7df03a5..0000000000
--- 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