diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 11:49:16 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 11:49:16 +0100 |
| commit | f726e860917b56abc94f21d9d5add7594d23bb6d (patch) | |
| tree | 20ed3691c55ae835ec387a836f5e08a9eacb563e | |
| parent | 883736f0158d47f9999250eb977cab5a55bb1fc9 (diff) | |
| parent | 2c39047fc52ce2e8df6e93121a867dc8d3026b80 (diff) | |
Merge PR #6854: comment "resolvability" bit in Evd.evar_map
| -rw-r--r-- | pretyping/typeclasses.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ee28ec173..b27e05938 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -93,7 +93,12 @@ val no_goals : evar_filter val no_goals_or_obligations : evar_filter (** Resolvability. - Only undefined evars can be marked or checked for resolvability. *) + Only undefined evars can be marked or checked for resolvability. + They represent type-class search roots. + + A resolvable evar is an evar the type-class engine may try to solve + An unresolvable evar is an evar the type-class engine will NOT try to solve +*) val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t val is_resolvable : evar_info -> bool |