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/evd.mli | |
| parent | 4ffb04be9b8829abb0f869fb4fd68156f4a01f95 (diff) | |
| parent | 00a75503ed7c7bcffb7a7e0bbb6cf4255d83255b (diff) | |
Merge PR #8852: Use the obligation evar flag
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 *) |