X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=d04acd181ba2c7c621b00ec2f479f2089aaafebe;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=8d42450685d2ec18287ad1deb1d299b43ea2f157;hpb=9352c5815be42fadc2c1f0241c0449a56273fd12;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 8d4245068..d04acd181 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -933,24 +933,26 @@ 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_and_matched_term_list =
   match what with
-     None -> context, where
+     None -> [context, where]
    | Some what ->
-      try
+      let res =
        ProofEngineHelpers.locate_in_term
         ~equality:first_is_the_expandable_head_of_second
         what ~where context
-      with
-       ProofEngineHelpers.TermNotFound ->
+      in
+       if res = [] then
         raise
          (ProofEngineTypes.Fail
            ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+       else
+        res
  in
-  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
+  let reduced_terms =
+   List.map
+    (function (context,where) -> hd_delta_beta context [] where)
+    context_and_matched_term_list in
+  let whats = List.map snd context_and_matched_term_list in
+   replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
 ;;