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 a9b8b55001a47c5ee3390b9556c90f1c4ec642c8..d04acd181ba2c7c621b00ec2f479f2089aaafebe 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,19 +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
-  hd_delta_beta context [] 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
 ;;