From 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 Oct 2018 22:04:38 +0100
Subject: Switch to using the obligation_evar flag instead of the evar source

for the determination of evars that can be turned into obligations.
---
 engine/evd.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/evd.mli')

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 *)
 
-- 
cgit v1.2.3