Another correction to the dependent existential variable printing

for emacs mode.

Hopefully fixes Bug 2678 this time. Much saner and more compact code.

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

1 files changed, 10 insertions, 12 deletions

diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 77985c8d7..41e8e0e18 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -120,21 +120,19 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr
 
 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
-
+(** [gather_dependent_evars evm seeds] classifies the evars in [evm]
+    as dependent_evars and goals (these may overlap). A goal is an
+    evar in [seeds] or an evar appearing in the (partial) definition
+    of a goal. A dependent evar is an evar appearing in the type
+    (hypotheses and conclusion) of a goal, or in the type or (partial)
+    definition of a dependent evar.  The value return is a map
+    associating to each dependent evar [None] if it has no (partial)
+    definition or [Some s] if [s] is the list of evars appearing in
+    its (partial) definition. *)
+val gather_dependent_evars : 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.