From cae62c87e2a361aeb31d3382280e5d7f18126e92 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 12 Jul 2007 17:15:22 +0000
Subject: 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
---
 contrib/setoid_ring/Ring_zdiv.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/setoid_ring/Ring_zdiv.v b/contrib/setoid_ring/Ring_zdiv.v
index 10141b6b4b..9b102c28c8 100644
--- a/contrib/setoid_ring/Ring_zdiv.v
+++ b/contrib/setoid_ring/Ring_zdiv.v
@@ -66,7 +66,7 @@ Ltac ztac := repeat (rewrite Zmult_plus_distr_l ||
 
 Theorem pdiv_eucl_correct: forall a b,
   let (q,r) := pdiv_eucl a b in Zpos a = (Z_of_N q * Zpos b + Z_of_N r)%Z.
-induction a; unfold pdiv_eucl; fold pdiv_eucl.
+induction a; cbv beta iota delta [pdiv_eucl]; fold pdiv_eucl; cbv zeta.
   intros b; generalize (IHa b); case pdiv_eucl.
     intros q1 r1 Hq1.
      generalize (Ngeb_correct (2 * r1 + 1) b); case Ngeb; intros H.
-- 
cgit v1.2.3