From 2c39047fc52ce2e8df6e93121a867dc8d3026b80 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 27 Feb 2018 16:38:25 +0100
Subject: comment "resolvability" bit in Evd.evar_map

---
 pretyping/typeclasses.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ee28ec173b..b27e05938b 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
-- 
cgit v1.2.3