diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-27 16:38:25 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-27 23:13:54 +0100 |
| commit | 2c39047fc52ce2e8df6e93121a867dc8d3026b80 (patch) | |
| tree | d30f7a9b252fd900c9a52f48366e170a94393d5a /pretyping | |
| parent | e3124e098ef8170dac2b348b91757a7034bc4999 (diff) | |
comment "resolvability" bit in Evd.evar_map
Diffstat (limited to 'pretyping')
| -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 |