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/termops.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'engine/termops.ml')

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