diff options
| author | Pierre-Marie Pédrot | 2018-11-03 16:14:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 16:14:49 +0100 |
| commit | 228066a783a581ba2b304a12d9fe5e8decebcc48 (patch) | |
| tree | df03e7a95d544d42a44b5c464938a8925ec80cfc /engine/termops.ml | |
| parent | 4ffb04be9b8829abb0f869fb4fd68156f4a01f95 (diff) | |
| parent | 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (diff) | |
Merge PR #8852: Use the obligation evar flag
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 8 |
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 |