Uniformisation (Qed/Save et Implicits Arguments)

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

1 files changed, 8 insertions, 8 deletions

diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index 739ead5e0..cbd8d9e4e 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.