Adds a pair of function in Evar_util to gather dependent evars in an

[evar_map].

We also gather some metadata on these evars: if they are still undefined,
and if not, which evars have been used in their (partial) instantiation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14720 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index c0c4252e6..36e64c9ad 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -110,10 +110,25 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr
 (** The following functions return the set of evars immediately
     contained in the object, including defined evars *)
 
+
 val evars_of_term : constr -> Intset.t
+
+(** returns the evars contained in the term associated with
+    the evars they contain themselves in their body, if any.
+    If the evar has no body, [None] is associated to it. *)
+val evars_of_evars_of_term : evar_map -> constr -> (Intset.t option) Intmap.t
 val evars_of_named_context : named_context -> Intset.t
 val evars_of_evar_info : evar_info -> Intset.t
 
+(** returns the evars which can be found in the typing context of the argument evars,
+    in the same format as {!evars_of_evars_of_term}.
+    It explores recursively the evars in the body of the argument evars -- but does
+    not return them. *)
+(* spiwack: tongue in cheek: it should have been called
+    [evars_of_evars_in_types_of_list_and_recursively_in_bodies] *)
+val evars_of_evars_in_types_of_list : evar_map -> evar list -> (Intset.t option) Intmap.t
+
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and