aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-27 16:38:25 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-27 23:13:54 +0100
commit2c39047fc52ce2e8df6e93121a867dc8d3026b80 (patch)
treed30f7a9b252fd900c9a52f48366e170a94393d5a /pretyping
parente3124e098ef8170dac2b348b91757a7034bc4999 (diff)
comment "resolvability" bit in Evd.evar_map
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/typeclasses.mli7
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