1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 8d42450685d2ec18287ad1deb1d299b43ea2f157..d04acd181ba2c7c621b00ec2f479f2089aaafebe 100644 (file)
--- 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
 ;;