aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index f720e5195d..181efa0ade 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -366,12 +366,18 @@ let pr_evar_map_gen with_univs pr_evars env 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 env sigma
in
- evs ++ svs ++ cstrs ++ typeclasses ++ metas
+ evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas
let pr_evar_list env sigma l =
let open Evd in