Module Ssripats.Internal

val examine_abstract : EConstr.t -> Goal.goal Evd.sigma -> EConstr.types * EConstr.t array
val pf_find_abstract_proof : bool -> Goal.goal Evd.sigma -> Constr.constr -> Evar.t