X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=22b6c8487a8348d74a80f896c501a26f3263aba1;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=c24ccc773cf35f14138464bb639a9e5015e19739;hpb=961a5b5095b72f566fd1412267ef68a820d5aa3d;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index c24ccc773..22b6c8487 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -554,15 +554,17 @@ exception Fail of string
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
-(** locate_in_term what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_term what ~where context =
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+*)
+let locate_in_term ?(equality=(==))what ~where context =
   let add_ctx context name entry =
-      (Some (name, entry)) :: context
-  in
+      (Some (name, entry)) :: context in
   let rec aux context where =
-   if what == where then context
+   if equality what where then [context,where]
    else
     match where with
     | Cic.Implicit _
@@ -605,10 +607,13 @@ let locate_in_term what ~where context =
   in
    aux context where
 
-(** locate_in_conjecture what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_conjecture what (_,context,ty) =
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+*)
+let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
  let context,res =
   List.fold_right
    (fun entry (context,res) ->
@@ -623,14 +628,14 @@ let locate_in_conjecture what (_,context,ty) =
          let res =
           match ty with
              None -> res
-           | Some ty -> res @ locate_in_term what ~where:ty context in
+           | Some ty ->
+              res @ locate_in_term what ~where:ty context in
          let context' = entry::context in
           context',res
    ) context ([],[])
  in
   res @ locate_in_term what ~where:ty context
 
-
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)
 (* which there is new a META for each hypothesis, a list of arguments for the *)