Uniformisation (Qed/Save et Implicits Arguments)

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

6 files changed, 45 insertions, 45 deletions

diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index 739ead5e0c..cbd8d9e4e3 100644
--- a/theories/Num/AddProps.v
+++ b/theories/Num/AddProps.v
@@ -14,44 +14,44 @@ Require Export EqAxioms.
 (** Properties of Addition *)
 Lemma add_x_0 : (x:N)(x+zero)=x.
 EAuto 3 with num.
-Save.
+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.
-Save.
+Qed.
 
 Hints Resolve add_x_Sy : num.
 
 Lemma add_x_Sy_swap : (x,y:N)(x+(S y))=((S x)+y).
 EAuto with num.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+Qed.
 Hints Resolve add_one_x_S : num.
 
 
diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v
index fd578ad17a..fe787589a1 100644
--- a/theories/Num/DiscrProps.v
+++ b/theories/Num/DiscrProps.v
@@ -15,5 +15,5 @@ Require Export LtProps.
 
 Lemma lt_le_Sx_y : (x,y:N)(x<y) -> ((S x)<=y).
 EAuto with num.
-Save.
+Qed.
 Hints Resolve lt_le_Sx_y : num.
\ No newline at end of file
diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v
index bf7af0d667..9703ec77f7 100644
--- a/theories/Num/LeProps.v
+++ b/theories/Num/LeProps.v
@@ -13,18 +13,18 @@ Require Export LeAxioms.
 
 Lemma lt_le : (x,y:N)(x<y)->(x<=y).
 Auto with num.
-Save.
+Qed.
 
 Lemma eq_le : (x,y:N)(x=y)->(x<=y).
 Auto with num.
-Save.
+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.
-Save.
+Qed.
 Hints Resolve le_eq_compat : num.
 
 (** Transitivity *)
@@ -33,31 +33,31 @@ 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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+Qed.
 Hints Resolve le_S_compat : num.
 
 
@@ -65,39 +65,39 @@ Hints Resolve le_S_compat : num.
 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.
-Save.
+Qed.
 Hints Immediate le_lt_x_Sy : num.
 
 Lemma le_le_x_Sy : (x,y:N)(x<=y)->(x<=(S y)).
 Auto with num.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+Qed.
 Hints Immediate lt_add_compat_weak_r : num.
 
 
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
index 9b77b38939..511859efb1 100644
--- a/theories/Num/LtProps.v
+++ b/theories/Num/LtProps.v
@@ -15,68 +15,68 @@ Require Export NeqProps.
 
 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.
-Save.
+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.
-Save.
+Qed.
 Hints Resolve eq_not_lt : num.
 
 Lemma lt_0_1 : (zero<one).
 EAuto with num.
-Save.
+Qed.
 Hints Resolve lt_0_1 : num.
 
 
 Lemma eq_lt_x_Sy : (x,y:N)(x=y)->(x<(S y)).
 EAuto with num.
-Save.
+Qed.
 Hints Resolve eq_lt_x_Sy : num.
 
 Lemma lt_lt_x_Sy : (x,y:N)(x<y)->(x<(S y)).
 EAuto with num.
-Save.
+Qed.
 Hints Immediate lt_lt_x_Sy : num.
 
 Lemma lt_Sx_y_lt : (x,y:N)((S x)<y)->(x<y).
 EAuto with num.
-Save.
+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.
-Save.
+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.
-Save.
+Qed.
 Hints Immediate lt_neq_sym : num.
 
 (** Application to inequalities properties *)
 
 Lemma neq_x_Sx : (x:N)x<>(S x).
 Auto with num.
-Save.
+Qed.
 Hints Resolve neq_x_Sx : num.
 
 Lemma neq_0_1 : zero<>one.
 Auto with num.
-Save.
+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.
-Save.
+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.
-Save.
+Qed.
 Hints Immediate lt_add_compat : num.
 
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
index c13f262472..9d310a0398 100644
--- a/theories/Num/NeqDef.v
+++ b/theories/Num/NeqDef.v
@@ -20,17 +20,17 @@ Infix 6 "<>" neq.
 (* Proofs of axioms *)
 Lemma eq_not_neq : (x,y:N)x=y->~(x<>y).
 Unfold neq; Auto with num.
-Save.
+Qed.
 Hints Immediate eq_not_neq : num.
 
 Lemma neq_sym : (x,y:N)(x<>y)->(y<>x).
 Unfold neq; Auto with num.
-Save.
+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.
-Save.
+Qed.
 Hints Resolve neq_not_neq_trans : num.
 
 
diff --git a/theories/Num/NeqProps.v b/theories/Num/NeqProps.v
index 6109c1f801..73f6066ab7 100644
--- a/theories/Num/NeqProps.v
+++ b/theories/Num/NeqProps.v
@@ -16,33 +16,33 @@ Require Export EqAxioms.
 
 Lemma neq_antirefl : (x:N)~(x<>x).
 Auto with num.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+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.
-Save.
+Qed.