aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-03 16:14:49 +0100
committerPierre-Marie Pédrot2018-11-03 16:14:49 +0100
commit228066a783a581ba2b304a12d9fe5e8decebcc48 (patch)
treedf03e7a95d544d42a44b5c464938a8925ec80cfc /engine/evd.ml
parent4ffb04be9b8829abb0f869fb4fd68156f4a01f95 (diff)
parent00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (diff)
Merge PR #8852: Use the obligation evar flag
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml2
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