(** 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
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 *)