locate_in_term generalized to locate_in_conjecture

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 4bb46fc4c011c491abfd316271b6e2b968137413..c24ccc773cf35f14138464bb639a9e5015e19739 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -557,7 +557,7 @@ exception Fail of string
 (** 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 =
+let locate_in_term what ~where context =
   let add_ctx context name entry =
       (Some (name, entry)) :: context
   in
@@ -603,7 +603,32 @@ let locate_in_term what ~where =
   and auxs context tl =  (* as aux for list of terms *)
     List.concat (List.map (fun t -> aux context t) tl)
   in
-   aux [] where
+   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) =
+ let context,res =
+  List.fold_right
+   (fun entry (context,res) ->
+     match entry with
+        None -> entry::context, res
+      | Some (_, Cic.Decl ty) ->
+         let res = res @ locate_in_term what ~where:ty context in
+         let context' = entry::context in
+          context',res
+      | Some (_, Cic.Def (bo,ty)) ->
+         let res = res @ locate_in_term what ~where:bo context in
+         let res =
+          match ty with
+             None -> res
+           | 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                                  *)