fold travaille maintenant sur la forme beta-iota-zeta réduite du

corps de la constante (comme unfold le fait ici), de telle sorte que
"unfold f; fold f" marche (cf bug 1789)



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

3 files changed, 18 insertions, 4 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 01d31441d6..2ee2443ffc 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -165,12 +165,15 @@ let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
 let betaiota = mkflags [fBETA;fIOTA]
 let beta = mkflags [fBETA]
 let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
+
+(* Removing fZETA for finer behaviour would break many developments *)
+let unfold_side_flags = [fBETA;fIOTA;fZETA]
+let unfold_side_red = mkflags [fBETA;fIOTA;fZETA]
 let unfold_red kn = 
   let flag = match kn with
     | EvalVarRef id -> fVAR id
-    | EvalConstRef kn -> fCONST kn
-  in (* Remove fZETA for finer behaviour ? *)
-  mkflags [fBETA;flag;fIOTA;fZETA]
+    | EvalConstRef kn -> fCONST kn in
+  mkflags (flag::unfold_side_flags)
 
 (************************* Obsolète
 (* [r_const=(true,cl)] means all constants but those in [cl] *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index ea8bccede8..926e152e04 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -76,6 +76,7 @@ val betadeltaiota      : reds
 val betaiotazeta       : reds
 val betadeltaiotanolet : reds
 
+val unfold_side_red : reds
 val unfold_red : evaluable_global_reference -> reds
 
 (***********************************************************************)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 60664f1994..3ee82a6857 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -801,7 +801,17 @@ let fold_one_com com env sigma c =
   let rcom =
     try red_product env sigma com
     with Redelimination -> error "Not reducible" in
-  subst1 com (subst_term rcom c)
+  (* Reason first on the beta-iota-zeta normal form of the constant as
+     unfold produces it, so that the "unfold f; fold f" configuration works
+     to refold fix expressions *)
+  let a = subst_term (clos_norm_flags unfold_side_red env sigma rcom) c in
+  if not (eq_constr a c) then
+    subst1 com a
+  else
+    (* Then reason on the non beta-iota-zeta form for compatibility -
+       even if it is probably a useless configuration *)
+    let a = subst_term rcom c in
+    subst1 com a
 
 let fold_commands cl env sigma c =
   List.fold_right (fun com -> fold_one_com com env sigma) (List.rev cl) c