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/evd.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/evd.ml')
| -rw-r--r-- | engine/evd.ml | 2 |
1 files changed, 2 insertions, 0 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 |