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 =
let add_ctx context name entry =
(Some (name, entry)) :: context