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.ml     | 2 ++
 engine/evd.mli    | 3 +++
 engine/termops.ml | 8 +++++++-
 3 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 3a77a2b440..b3848e1b5b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -483,6 +483,8 @@ let is_typeclass_evar evd evk =
   let flags = evd.evar_flags in
   Evar.Set.mem evk flags.typeclass_evars
 
+let get_obligation_evars evd = evd.evar_flags.obligation_evars
+
 let set_obligation_evar evd evk =
   let flags = evd.evar_flags in
   let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
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 *)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 5e220fd8f1..bd4021192c 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -371,12 +371,18 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     else
       str "TYPECLASSES:" ++ brk (0, 1) ++
       prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
+  and obligations =
+    let evars = Evd.get_obligation_evars sigma in
+    if Evar.Set.is_empty evars then mt ()
+    else
+      str "OBLIGATIONS:" ++ brk (0, 1) ++
+      prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
   in
-  evs ++ svs ++ cstrs ++ typeclasses ++ metas
+  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas
 
 let pr_evar_list sigma l =
   let open Evd in
-- 
cgit v1.2.3