Uniformisation (Qed/Save et Implicits Arguments)

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

8 files changed, 30 insertions, 30 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index f9e93b9bf9..d729253b3d 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -15,7 +15,7 @@ Require Decidable.
 
 Theorem zerop : (n:nat){n=O}+{lt O n}.
 NewDestruct n; Auto with arith.
-Save.
+Qed.
 
 Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
 Proof.
@@ -61,42 +61,42 @@ Theorem dec_le:(x,y:nat)(decidable (le x y)).
 Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [
   Auto with arith
 | Intro; Right; Apply gt_not_le; Assumption].
-Save.
+Qed.
 
 Theorem dec_lt:(x,y:nat)(decidable (lt x y)).
 Intros x y; Unfold lt; Apply dec_le.
-Save.
+Qed.
 
 Theorem dec_gt:(x,y:nat)(decidable (gt x y)).
 Intros x y; Unfold gt; Apply dec_lt.
-Save.
+Qed.
 
 Theorem dec_ge:(x,y:nat)(decidable (ge x y)).
 Intros x y; Unfold ge; Apply dec_le.
-Save.
+Qed.
 
 Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x).
 Intros x y H; Elim (lt_eq_lt_dec x y); [
   Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption]
 | Auto with arith].
-Save.
+Qed.
 
 
 Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y).
 Intros x y H; Elim (le_gt_dec x y);
   [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ].
-Save.
+Qed.
 
 Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y).
 Intros x y H; Elim (le_gt_dec x y);
   [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption].
-Save.
+Qed.
 
 Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y).
 Intros x y H; Exact (not_le y x H).
-Save.
+Qed.
 
 Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y).
 Intros x y H; Exact (not_gt y x H). 
-Save.
+Qed.
 
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index 718a516139..2b7cfac144 100755
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -37,7 +37,7 @@ Simpl.
 Elim plus_n_O; Auto with arith.
 Apply le_antisym; Auto with arith.
 Elim plus_n_Sm; Auto with arith.
-Save.
+Qed.
 
 Theorem div2 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
 Realizer Fix div1 {div1/2: nat->nat->diveucl :=
@@ -56,4 +56,4 @@ Simpl.
 Elim plus_n_O; Auto with arith.
 Apply le_antisym; Auto with arith.
 Elim plus_n_Sm; Auto with arith.
-Save.
+Qed.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index c6db2917bd..5a2dd1a84e 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -28,7 +28,7 @@ Elim plus_assoc_l.
 Elim e; Auto with arith.
 Intros gtbn.
 Apply divex with O n; Simpl; Auto with arith.
-Save.
+Qed.
 
 Lemma quotient : (b:nat)(gt b O)->
      (a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}.
@@ -43,7 +43,7 @@ Elim plus_assoc_l.
 Elim H1; Auto with arith.
 Intros gtbn.
 Exists O; Exists n; Simpl; Auto with arith.
-Save.
+Qed.
 
 Lemma modulo : (b:nat)(gt b O)->
      (a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}.
@@ -58,4 +58,4 @@ Elim plus_assoc_l.
 Elim H1; Auto with arith.
 Intros gtbn.
 Exists n; Exists O; Simpl; Auto with arith.
-Save.
+Qed.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index be935d88cf..074e0a03d1 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -26,21 +26,21 @@ Proof.
 NewInduction n.
 Auto with arith.
 Elim IHn; Auto with arith.
-Save.
+Qed.
 
 Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }.
 Proof.
 NewInduction n.
 Auto with arith.
 Elim IHn; Auto with arith.
-Save.
+Qed.
 
 Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
 Proof.
 NewInduction n.
 Intros. Inversion H0.
 Intros. Inversion H. Inversion H0. Auto with arith.
-Save.
+Qed.
 
 Lemma even_plus_aux:
   (n,m:nat)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index e6a448a8ea..711e065da9 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -61,7 +61,7 @@ Hints Immediate lt_pred : arith v62.
 
 Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
 NewDestruct 1; Simpl; Auto with arith.
-Save.
+Qed.
 Hints Resolve lt_pred_n_n : arith v62.
 
 (** Relationship between [le] and [lt] *) 
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 417629621e..0f435a5602 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -50,7 +50,7 @@ Hints Immediate plus_minus : arith v62.
 
 Lemma minus_plus : (n,m:nat)(minus (plus n m) n)=m.
 Symmetry; Auto with arith.
-Save.
+Qed.
 Hints Resolve minus_plus : arith v62.
 
 Lemma le_plus_minus : (n,m:nat)(le n m)->(m=(plus n (minus m n))).
@@ -93,7 +93,7 @@ Hints Immediate lt_O_minus_lt : arith v62.
 
 Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
 NewInduction x; Auto with arith.
-Save.
+Qed.
 
 
 Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O.
@@ -102,4 +102,4 @@ Intros y x; Pattern y x ; Apply nat_double_ind; [
 | Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n]
 | Simpl; Intros n m H1 H2; Apply H1;
   Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption].
-Save.
+Qed.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index c7e6a4f1da..ac16d4cb9f 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.
 
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 16aa58afac..e8e91670b7 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -100,7 +100,7 @@ Apply Acc_intro.
 Intros b ltfafb.
 Apply IHn.
 Apply lt_le_trans with (f a); Auto with arith.
-Save.
+Qed.
 
 End Well_founded_Nat.
 
@@ -120,7 +120,7 @@ Proof [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
 Lemma lt_wf_ind : (p:nat)(P:nat->Prop)
               ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
 Intros; Elim (lt_wf p); Auto with arith.
-Save.
+Qed.
 
 Lemma gt_wf_rec : (p:nat)(P:nat->Set)
               ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
@@ -136,7 +136,7 @@ Lemma lt_wf_double_rec :
    -> (p,q:nat)(P p q).
 Intros P Hrec p; Pattern p; Apply lt_wf_rec.
 Intros; Pattern q; Apply lt_wf_rec; Auto with arith.
-Save.
+Qed.
 
 Lemma lt_wf_double_ind : 
   (P:nat->nat->Prop)
@@ -144,7 +144,7 @@ Lemma lt_wf_double_ind :
    -> (p,q:nat)(P p q).
 Intros P Hrec p; Pattern p; Apply lt_wf_ind.
 Intros; Pattern q; Apply lt_wf_ind; Auto with arith.
-Save.
+Qed.
 
 Hints Resolve lt_wf : arith.
 Hints Resolve well_founded_lt_compat : arith.