+ metasenv:Cic.metasenv ->
+ ugraph:CicUniv.universe_graph ->
+ conjecture:Cic.conjecture ->
+ pattern:ProofEngineTypes.pattern ->
+ Cic.substitution * Cic.metasenv * CicUniv.universe_graph *
+ [ `Decl of (Cic.context * Cic.term) list
+ | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option
+ ] option list *
+ (Cic.context * Cic.term) list
+
+(** 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]
+*)
+val locate_in_term:
+ ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term ->
+ Cic.context -> (Cic.context * Cic.term) list
+
+(** 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]
+*)
+val locate_in_conjecture:
+ ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture ->