diff options
| author | Matthieu Sozeau | 2018-10-29 22:04:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-30 11:45:05 +0100 |
| commit | 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (patch) | |
| tree | d15e9319ecc1fb41059acba55328d393a66acfb9 /engine/termops.ml | |
| parent | 57a0d5091a9524d35161875a884835a573d82e0b (diff) | |
Switch to using the obligation_evar flag instead of the evar source
for the determination of evars that can be turned into obligations.
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 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 |