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

7 files changed, 33 insertions, 20 deletions

diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index c4ec7baf8d..470130b9b8 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.
-Omega. (* Auto with zarith. *)
+Auto with zarith.
 Unfold Zpred; Omega.
 Save.
 
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index c696aec28c..52f7117153 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
-  (Cases q of
+  (<Z*Z>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 4d8e3092ac..5a4bd252e5 100755
--- a/dev/ocamldebug-v7
+++ b/dev/ocamldebug-v7
@@ -3,7 +3,7 @@
 # wrap around ocamldebug for Coq
 
 # export COQTOP=`coqtop -where`
-export COQTOP=$HOME/coq/V7
+export COQTOP=`pwd`
 export COQLIB=$COQTOP
 export COQTH=$COQLIB/theories
 export CAMLP4LIB=`camlp4 -where`
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c169e9d18a..71edc098a6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -109,6 +109,7 @@ let stack_reduction_of_reduction red_fun env sigma s =
   let t = red_fun env sigma (app_stack s) in
   whd_stack t
 
+(* BUGGE : NE PREND PAS EN COMPTE LES DEFS LOCALES *)
 let strong whdfun env sigma = 
   let rec strongrec t = map_constr strongrec (whdfun env sigma t) in
   strongrec
@@ -270,9 +271,19 @@ let reduce_fix whdfun fix stack =
 let whd_state_gen flags env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
+(*
+      | IsRel n when red_delta flags ->
+	  (match lookup_rel_value n env with
+	     | Some body -> whrec (lift n body, stack)
+	     | None -> s)
+      | IsVar id when red_delta flags ->
+	  (match lookup_var_value id env with
+	     | Some body -> whrec (body, stack)
+	     | None -> s)
+*)
       | IsEvar ev when red_evar flags ->
 	  (match existential_opt_value sigma ev with
-	     | Some  body -> whrec (body, stack)
+	     | Some body -> whrec (body, stack)
 	     | None -> s)
       | IsConst const when red_delta flags ->
 	  (match constant_opt_value env const with
@@ -1199,7 +1210,7 @@ let rec whd_ise1 sigma c =
     *)
     | _ -> c
 
-let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma
+let nf_ise1 sigma = local_strong (whd_ise1 sigma)
 
 (* A form of [whd_ise1] with type "reduction_function" *)
 let whd_evar env = whd_ise1
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 5520e179d8..a2187a89bc 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 a79a4d2672..e2ae8eed27 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 d1f45be08e..86fd7c9ec2 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.