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, 4 insertions, 4 deletions

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index c7e6a4f1d..ac16d4cb9 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -51,24 +51,24 @@ Hints Resolve mult_assoc_r : arith v62.
 
 Lemma mult_assoc_l : (n,m,p:nat)(mult n (mult m p)) = (mult (mult n m) p).
 Auto with arith.
-Save.
+Qed.
 Hints Resolve mult_assoc_l : arith v62.
 
 Lemma mult_1_n : (n:nat)(mult (S O) n)=n.
 Simpl; Auto with arith.
-Save.
+Qed.
 Hints Resolve mult_1_n : arith v62.
 
 Lemma mult_sym : (n,m:nat)(mult n m)=(mult m n).
 Intros; Elim n; Intros; Simpl; Auto with arith.
 Elim mult_n_Sm.
 Elim H; Apply plus_sym.
-Save.
+Qed.
 Hints Resolve mult_sym : arith v62.
 
 Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
 Intro; Elim mult_sym; Auto with arith.
-Save.
+Qed.
 Hints Resolve mult_n_1 : arith v62.