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 | |
| 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')
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 3 | ||||
| -rw-r--r-- | engine/termops.ml | 8 |
3 files changed, 12 insertions, 1 deletions
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 |