Mise en conformité nouveau Simpl pour Fix

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

3 files changed, 17 insertions, 15 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 5520e179d..a2187a89b 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -27,7 +27,7 @@ Intros. Elim (H2 n). Auto with arith.
 
 Induction n0. Auto with arith.
 Intros. Elim H2; Auto with arith.
-Save.
+Qed.
 
 (* 0 <n  =>  n/2 < n *)
 
@@ -40,7 +40,7 @@ Intros. Simpl.
 Case (zerop n0).
 Intro. Rewrite e. Auto with arith.
 Auto with arith.
-Save.
+Qed.
 
 Hints Resolve lt_div2 : arith.
 
@@ -67,7 +67,7 @@ Intro H. Inversion H. Inversion H1.
 Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith.
 Intro H. Inversion H. Inversion H1.
 Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith.
-Save.
+Qed.
 
 (* Specializations *)
 
@@ -94,7 +94,7 @@ Hints Unfold double : arith.
 Lemma double_S : (n:nat) (double (S n))=(S (S (double n))).
 Proof.
 Intro. Unfold double. Simpl. Auto with arith.
-Save.
+Qed.
 
 Hints Resolve double_S : arith.
 
@@ -113,12 +113,12 @@ Intros. Decompose [and] H. Unfold iff in H0 H1.
 Decompose [and] H0. Decompose [and] H1. Clear H H0 H1.
 Split; Split.
 Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
-Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
+Simpl. Rewrite <- plus_n_Sm. Auto with arith.
+Simpl. Rewrite <- plus_n_Sm. Intro H. Injection H. Auto with arith.
 Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
-Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
-Save.
+Simpl. Rewrite <- plus_n_Sm. Auto with arith.
+Simpl. Rewrite <- plus_n_Sm. Intro H. Injection H. Auto with arith.
+Qed.
 
 
 (* Specializations *)
@@ -147,10 +147,10 @@ Hints Resolve even_double double_even odd_double double_odd : arith.
 Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }.
 Proof.
 Intros n H. Exists (div2 n). Auto with arith.
-Save.
+Qed.
 
 Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }.
 Proof.
 Intros n H. Exists (div2 n). Auto with arith.
-Save.
+Qed.
 
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index a79a4d267..e2ae8eed2 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -30,7 +30,7 @@ Auto with arith.
 Intros n' H. Elim H; Auto with arith.
 Save.
 
-Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
+Lemma not_even_and_odd2 : (n:nat) (even n) -> (odd n) -> False.
 Proof.
 Induction n.
 Intros. Inversion H0.
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index d1f45be08..86fd7c9ec 100755
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -46,7 +46,7 @@ Lemma eq_dep_dep1 : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y)
 Proof.
 Induction 1; Intros.
 Apply eq_dep1_intro with (refl_equal U p).
-Elim eq_rec_eq; Trivial.
+Simpl. Trivial.
 Qed.
 
 Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y.
@@ -60,7 +60,7 @@ Proof.
 Intros; Apply eq_dep1_eq; Apply eq_dep_dep1; Trivial.
 Qed.
 
-Lemma equiv_eqex_eqdep : (p,q:U)(x:(P p))(y:(P q)) 
+Lemma equiv_eqex_eq_dep : (p,q:U)(x:(P p))(y:(P q)) 
     (existS U P p x)=(existS U P q y) <-> (eq_dep p x q y).
 Proof.
 Split. 
@@ -79,13 +79,15 @@ Elim H.
 Auto.
 Qed.
 
+(* For compatibility *)
+Syntactic Definition equiv_eqex_eqdep := equiv_eqex_eq_dep.
 
 Lemma inj_pair2: (p:U)(x,y:(P p))
     (existS U P p x)=(existS U P p y)-> x=y.
 Proof.
 Intros.
 Apply eq_dep_eq.
-Generalize (equiv_eqex_eqdep p p x y) .
+Generalize (equiv_eqex_eq_dep p p x y) .
 Induction 1.
 Intros.
 Auto.