Commit malencontreux sur précédente version

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

5 files changed, 7 insertions, 9 deletions

diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index 470130b9b8..c4ec7baf8d 100644
--- a/contrib/omega/Zcomplements.v
+++ b/contrib/omega/Zcomplements.v
@@ -84,7 +84,7 @@ Simpl; Do 2 Rewrite Zmult_n_1; Auto 1.
 Unfold Zs.
 Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r.
 Repeat Rewrite Zmult_n_1.
-Auto with zarith.
+Omega. (* Auto with zarith. *)
 Unfold Zpred; Omega.
 Save.
 
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index 52f7117153..c696aec28c 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -285,7 +285,7 @@ Section power_div_with_rest.
 Definition Zdiv_rest_aux :=
   [qrd:(Z*Z)*Z] 
   let (qr,d)=qrd in let (q,r)=qr in
-  (<Z*Z>Cases q of
+  (Cases q of
      ZERO => ` (0, r)`
    | (POS xH) => ` (0, d + r)`
    | (POS (xI n)) => ` ((POS n), d + r)`
diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7
index 5a4bd252e5..4d8e3092ac 100755
--- a/dev/ocamldebug-v7
+++ b/dev/ocamldebug-v7
@@ -3,7 +3,7 @@
 # wrap around ocamldebug for Coq
 
 # export COQTOP=`coqtop -where`
-export COQTOP=`pwd`
+export COQTOP=$HOME/coq/V7
 export COQLIB=$COQTOP
 export COQTH=$COQLIB/theories
 export CAMLP4LIB=`camlp4 -where`
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index e2ae8eed27..a79a4d2672 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_odd2 : (n:nat) (even n) -> (odd n) -> False.
+Lemma not_even_and_odd : (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 86fd7c9ec2..d1f45be08e 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).
-Simpl. Trivial.
+Elim eq_rec_eq; 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_eq_dep : (p,q:U)(x:(P p))(y:(P q)) 
+Lemma equiv_eqex_eqdep : (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,15 +79,13 @@ 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_eq_dep p p x y) .
+Generalize (equiv_eqex_eqdep p p x y) .
 Induction 1.
 Intros.
 Auto.