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 a9b8b55001a47c5ee3390b9556c90f1c4ec642c8..8d42450685d2ec18287ad1deb1d299b43ea2f157 100644 (file)
--- 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 ebb61a7c8bbb54ccf0094d050dfd8cdd8dc8a3a8..67247876aaa2e62f12a2bc5608f6c18f89d71487 100644 (file)
--- 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) ->