normalisation (by closure) was not performed under fixpoints

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

2 files changed, 11 insertions, 7 deletions

diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v
index 34b3b35e06..f404c92433 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Ints/num/GenDivn1.v
@@ -99,7 +99,7 @@ Section GENDIVN1.
   Proof.
    induction n;intros.
    exact (spec_div21 a b2p_le H).
-   unfold gen_divn1_0, gen_divn1_0_aux;fold gen_divn1_0.
+   simpl (gen_divn1_0 (S n) r a); unfold gen_divn1_0_aux.
    assert (H1 := spec_split n a);destruct (gen_split w_0 n a) as (hh,hl).
    rewrite H1.
    assert (H2 := IHn r hh H);destruct (gen_divn1_0 n r hh) as (qh,rh).
@@ -180,10 +180,12 @@ Section GENDIVN1.
   Proof.
    case (spec_to_Z p); intros HH0 HH1.
    induction n;intros.
-   unfold gen_divn1_p, gen_divn1_p_aux, gen_to_Z, gen_wB, gen_digits.
+   simpl (gen_divn1_p 0 r h l).
+   unfold gen_to_Z, gen_wB, gen_digits.
    rewrite <- spec_add_mul_divp.
    exact (spec_div21 (w_add_mul_div p h l) b2p_le H).
-   unfold gen_divn1_p,gen_divn1_p_aux;fold gen_divn1_p.
+   simpl (gen_divn1_p (S n) r h l).
+   unfold gen_divn1_p_aux.
    assert (H1 := spec_split n h);destruct (gen_split w_0 n h) as (hh,hl).
    rewrite H1. rewrite <- gen_wB_wwB.
    assert (H2 := spec_split n l);destruct (gen_split w_0 n l) as (lh,ll).
@@ -333,7 +335,7 @@ Section GENDIVN1.
   auto with zarith.
   assert (U0 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w0);
    assert (U1 := spec_gen_to_Z w_digits w_to_Z spec_to_Z n w1).
-  unfold gen_to_Z,zn2z_to_Z;fold (gen_to_Z w_digits w_to_Z).
+  simpl [!S n|WW w0 w1!].
   unfold gen_wB,base;rewrite Zdiv_shift_r;auto with zarith.
   replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos w_digits)) with
    (2^(Zpos (gen_digits w_digits n) - Zpos w_digits) * 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index d168b0369e..f9601b09a2 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* Contribution by Claude Marché and Xavier Urbain *)
+(* Contribution by Claude Marché and Xavier Urbain *)
 
 (** Euclidean Division
 
@@ -129,7 +129,8 @@ Lemma Z_div_mod_POS :
     forall a:positive,
       let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b.
 Proof.
-simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *.
+simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *;
+  fold Zdiv_eucl_POS in |- *; cbv zeta.
 
 intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1].
 generalize (Zgt_cases b (2 * r + 1)).
@@ -238,7 +239,8 @@ Qed.
 Lemma Z_div_POS_ge0 :
   forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0.
 Proof.
-  simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *.
+  simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *;
+    fold Zdiv_eucl_POS in |- *; cbv zeta.
   intro p; case (Zdiv_eucl_POS p b).
   intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega.
   intro p; case (Zdiv_eucl_POS p b).