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

1 files changed, 11 insertions, 1 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 60664f199..3ee82a685 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