From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Jul 2005 15:09:53 +0000 (+0000)
Subject: Bug fixed: unfold used to work iff the term to unfold was in head position in
X-Git-Tag: V_0_7_2~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9352c5815be42fadc2c1f0241c0449a56273fd12;p=helm.git

Bug fixed: unfold used to work iff the term to unfold was in head position in
the term.
---

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index a9b8b5500..8d4245068 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -127,7 +127,7 @@ let replace ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality t what then with_what else find_image_aux (tl1,tl2)
+        if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -190,7 +190,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality t what then with_what else find_image_aux (tl1,tl2)
+        if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -288,7 +288,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality t what then with_what else find_image_aux (tl1,tl2)
+        if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -933,7 +933,7 @@ let unfold ?what context where =
    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
    | t -> cannot_delta_expand t
  in
- let context, where =
+ let context, where' =
   match what with
      None -> context, where
    | Some what ->
@@ -947,5 +947,10 @@ let unfold ?what context where =
          (ProofEngineTypes.Fail
            ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
  in
-  hd_delta_beta context [] where
+  let reduced_term = hd_delta_beta context [] where' in
+   match what with
+      None -> reduced_term
+    | Some what ->
+       replace ~equality:first_is_the_expandable_head_of_second
+        ~what:[what] ~with_what:[reduced_term] ~where
 ;;
diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index ebb61a7c8..67247876a 100644
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -36,7 +36,7 @@ exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 val alpha_equivalence: Cic.term -> Cic.term -> bool
 val replace :
-  equality:(Cic.term -> 'a -> bool) ->
+  equality:('a -> Cic.term -> bool) ->
   what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val replace_lifting :
   equality:(Cic.term -> Cic.term -> bool) ->