Module Proofview.Progress

val goal_equal : evd:Evd.evar_map -> extended_evd:Evd.evar_map -> Evar.t -> Evar.t -> bool

goal_equal ~evd ~extended_evd evar extended_evar tests whether the evar_info from evd corresponding to evar is equal to that from extended_evd corresponding to extended_evar, up to existential variable instantiation and equalisable universes. The universe constraints in extended_evd are assumed to be an extension of the universe constraints in evd.