Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)

 After r13717, we concentrate on undefined evars. But doing so
 too naively was breaking Class_tactics.split_evars, since defined
 evars may point to undefined ones. We should not ignore them,
 but rather traverse them, which is now done by functions
 Evarutil.undefined_evars_of_*

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

2 files changed, 48 insertions, 0 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ae3f64b9cc..d1eb33cd6e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1359,6 +1359,9 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
   with e when precatchable_exception e ->
     (evd,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
@@ -1382,6 +1385,39 @@ let evars_of_evar_info evi =
 	| 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
+    [nf_evar]. *)
+
+let undefined_evars_of_term evd t =
+  let rec evrec acc c =
+    match kind_of_term c with
+      | Evar (n, _) -> (* TODO: should we look in the constr array ?? *)
+	(try match (Evd.find evd n).evar_body with
+	  | Evar_empty -> Intset.add n acc
+	  | Evar_defined c -> evrec acc c
+	 with Not_found -> anomaly "undefined_evars_of_term: evar not found")
+      | _ -> fold_constr evrec acc c
+  in
+  evrec Intset.empty t
+
+let undefined_evars_of_named_context evd nc =
+  List.fold_right (fun (_, b, t) s ->
+    Option.fold_left (fun s t ->
+      Intset.union s (undefined_evars_of_term evd t))
+      (Intset.union s (undefined_evars_of_term evd t)) b)
+    nc Intset.empty
+
+let undefined_evars_of_evar_info evd evi =
+  Intset.union (undefined_evars_of_term evd evi.evar_concl)
+    (Intset.union
+       (match evi.evar_body with
+	 | Evar_empty -> Intset.empty
+	 | Evar_defined b -> undefined_evars_of_term evd b)
+       (undefined_evars_of_named_context evd
+	  (named_context_of_val evi.evar_hyps)))
+
 (* [check_evars] fails if some unresolved evar remains *)
 
 let check_evars env initial_sigma sigma c =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d3a2452de4..38da536834 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -96,10 +96,22 @@ val is_unification_pattern : env * int -> constr -> constr array ->
   constr -> bool
 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
 val evars_of_named_context : named_context -> Intset.t
 val evars_of_evar_info : evar_info -> Intset.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
+    [nf_evar]. *)
+
+val undefined_evars_of_term : evar_map -> constr -> Intset.t
+val undefined_evars_of_named_context : evar_map -> named_context -> Intset.t
+val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
+
 (** {6 Value/Type constraints} *)
 
 val judge_of_new_Type : unit -> unsafe_judgment