Switch to using the obligation_evar flag instead of the evar source

for the determination of evars that can be turned into obligations.

1 files changed, 3 insertions, 0 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index b0e3c2b869..be54bebcd7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -262,6 +262,9 @@ val get_typeclass_evars : evar_map -> Evar.Set.t
 val is_typeclass_evar : evar_map -> Evar.t -> bool
 (** Is the evar declared resolvable for typeclass resolution *)
 
+val get_obligation_evars : evar_map -> Evar.Set.t
+(** The set of obligation evars *)
+
 val set_obligation_evar : evar_map -> Evar.t -> evar_map
 (** Declare an evar as an obligation *)