Merging some functions from evarutil.ml/evd.ml.

- Removed collect_evars which does not consider instance
  (use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
  evars_of_filterered_evar_info instead). This is consistent with
  printing goal contexts in the filtered way.
  Anyway, as of today, afaics goals filters are trivial
  because (if I interpret evarutil.ml correctly), evars with
  non-trivial filter necessarily occur in a conv pb. Conversely,
  conv pbs being solved when tactics are called, there should not be
  an evar used as a goal with a non-trivial filter.

4 files changed, 61 insertions, 45 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7b1fee543..64bdb90a2 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -128,6 +128,11 @@ let nf_evar_map_undefined evm =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
+(* A probably faster though more approximative variant of
+   [has_undefined (nf_evar c)]: instances are not substituted and
+   maybe an evar occurs in an instance and it would disappear by
+   instantiation *)
+
 let has_undefined_evars evd t =
   let rec has_ev t =
     match kind_of_term t with
@@ -536,17 +541,6 @@ let clear_hyps2_in_evi evdref hyps t concl ids =
   | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
   | _ -> assert false
 
-(** The following functions return the set of evars immediately
-    contained in the object, including defined evars *)
-
-let evars_of_term c =
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
-    | _ -> fold_constr evrec acc c
-  in
-  evrec Evar.Set.empty c
-
 (* spiwack: a few functions to gather evars on which goals depend. *)
 let queue_set q is_dependent set =
   Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
@@ -594,21 +588,6 @@ let gather_dependent_evars evm l =
 
 (* /spiwack *)
 
-let evars_of_named_context nc =
-  List.fold_right (fun (_, b, t) s ->
-    Option.fold_left (fun s t ->
-      Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term t)) b)
-    nc Evar.Set.empty
-
-let evars_of_evar_info evi =
-  Evar.Set.union (evars_of_term evi.evar_concl)
-    (Evar.Set.union
-	(match evi.evar_body with
-	| Evar_empty -> Evar.Set.empty
-	| Evar_defined b -> evars_of_term b)
-	(evars_of_named_context (named_context_of_val evi.evar_hyps)))
-
 (** 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
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index b90a78434..8a07cce5d 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -82,8 +82,9 @@ val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
 (* Expand head evar if any *)
 val whd_head_evar :  evar_map -> constr -> constr
 
-(* [has_undefined_evars evd c] checks if [c] has undefined evars. *)
+(* An over-approximation of [has_undefined (nf_evars evd c)] *)
 val has_undefined_evars : evar_map -> constr -> bool
+
 val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 (** [check_evars env initial_sigma extended_sigma c] fails if some
@@ -101,15 +102,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
   evar_map * existential
 
-(** The following functions return the set of evars immediately
-    contained in the object, including defined evars *)
-
-
-val evars_of_term : constr -> Evar.Set.t
-
-val evars_of_named_context : named_context -> Evar.Set.t
-val evars_of_evar_info : evar_info -> Evar.Set.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
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 63e25a541..fd104d847 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -901,12 +901,10 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _ -> Loc.ghost
 
-let evar_list evd c =
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (evk, _ as ev) when mem evd evk -> ev :: acc
-    | _ -> fold_constr evrec acc c in
-  evrec [] c
+(** The following functions return the set of evars immediately
+    contained in the object *)
+
+(* including defined evars, excluding instances *)
 
 let collect_evars c =
   let rec collrec acc c =
@@ -916,6 +914,40 @@ let collect_evars c =
   in
   collrec Evar.Set.empty c
 
+(* including defined evars and instances of evars *)
+
+(* excluding defined evars *)
+
+let evar_list c =
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (evk, _ as ev) -> ev :: acc
+    | _ -> fold_constr evrec acc c in
+  evrec [] c
+
+let evars_of_term c =
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | _ -> fold_constr evrec acc c
+  in
+  evrec Evar.Set.empty c
+
+let evars_of_named_context nc =
+  List.fold_right (fun (_, b, t) s ->
+    Option.fold_left (fun s t ->
+      Evar.Set.union s (evars_of_term t))
+      (Evar.Set.union s (evars_of_term t)) b)
+    nc Evar.Set.empty
+
+let evars_of_filtered_evar_info evi =
+  Evar.Set.union (evars_of_term evi.evar_concl)
+    (Evar.Set.union
+	(match evi.evar_body with
+	| Evar_empty -> Evar.Set.empty
+	| Evar_defined b -> evars_of_term b)
+	(evars_of_named_context (evar_filtered_context evi)))
+
 (**********************************************************)
 (* Side effects *)
 
@@ -1669,7 +1701,7 @@ let compute_evar_dependency_graph (sigma : evar_map) =
     in
     match evar_body evi with
     | Evar_empty -> assert false
-    | Evar_defined c -> Evar.Set.fold fold_ev (collect_evars c) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
   in
   EvMap.fold fold sigma.defn_evars EvMap.empty
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index db4515ae8..22768fb69 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -82,6 +82,7 @@ type evar_body =
   | Evar_empty
   | Evar_defined of constr
 
+
 module Store : Store.S
 (** Datatype used to store additional information in evar maps. *)
 
@@ -374,8 +375,20 @@ val extract_changed_conv_pbs : evar_map ->
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
 val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
 
-val evar_list : evar_map -> constr -> existential list
-val collect_evars : constr -> Evar.Set.t
+(** The following functions return the set of evars immediately
+    contained in the object; need the term to be evar-normal otherwise
+    defined evars are returned too. *)
+
+val evar_list : constr -> existential list
+  (** excluding evars in instances of evars and collected with
+     redundancies from right to left (used by tactic "instantiate") *)
+
+val evars_of_term : constr -> Evar.Set.t
+  (** including evars in instances of evars *)
+
+val evars_of_named_context : named_context -> Evar.Set.t
+
+val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 
 (** Metas *)
 val meta_list : evar_map -> (metavariable * clbinding) list