Module `Proof.V82`

val background_subgoals : t -> Goal.goal list Evd.sigma
val top_goal : t -> Goal.goal Evd.sigma
val top_evars : t -> Evar.t list
val grab_evars : t -> t
val instantiate_evar : Environ.env -> int -> (Environ.env -> Evd.evar_map -> Glob_term.glob_constr) -> t -> t