From 6b01f89b083bf8acc666264222131d6ce2bb06bf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Mar 2008 21:52:06 +0000
Subject: 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
---
 pretyping/tacred.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3