+(** 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 add_ctx context name entry =
+ (Some (name, entry)) :: context
+ in
+ let rec aux context where =
+ if what == where then context
+ else
+ match where with
+ | Cic.Implicit _
+ | Cic.Meta _
+ | Cic.Rel _
+ | Cic.Sort _
+ | Cic.Var _
+ | Cic.Const _
+ | Cic.MutInd _
+ | Cic.MutConstruct _ -> []
+ | Cic.Cast (te, ty) -> aux context te @ aux context ty
+ | Cic.Prod (name, s, t)
+ | Cic.Lambda (name, s, t) ->
+ aux context s @ aux (add_ctx context name (Cic.Decl s)) t
+ | Cic.LetIn (name, s, t) ->
+ aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
+ | Cic.Appl tl -> auxs context tl
+ | Cic.MutCase (_, _, out, t, pat) ->
+ aux context out @ aux context t @ auxs context pat
+ | Cic.Fix (_, funs) ->
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
+ in
+ List.concat
+ (List.map
+ (fun (_, _, ty, bo) ->
+ aux context ty @ aux (tys @ context) bo)
+ funs)
+ | Cic.CoFix (_, funs) ->
+ let tys =
+ List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
+ in
+ List.concat
+ (List.map
+ (fun (_, ty, bo) ->
+ aux context ty @ aux (tys @ context) bo)
+ funs)
+ and auxs context tl = (* as aux for list of terms *)
+ List.concat (List.map (fun t -> aux context t) tl)
+ in
+ aux [] where
+
+