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

4 files changed, 54 insertions, 12 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
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4b1500ea91..6300c699ba 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -469,24 +469,18 @@ let rec merge_deps deps = function
 	merge_deps (Intset.union deps hd) tl
       else hd :: merge_deps deps tl
 
-let evars_of_evi evi evm =
-  Intset.filter (is_undefined evm)
-    (Intset.union
-       (Evarutil.evars_of_term evi.evar_concl)
-       (Evarutil.evars_of_named_context (evar_filtered_context evi)))
-
 let deps_of_constraints cstrs deps evm =
   List.fold_right (fun (_, _, x, y) deps ->
-    let evs =
-      Intset.filter (is_defined evm)
-	(Intset.union (Evarutil.evars_of_term x) (Evarutil.evars_of_term y))
-    in merge_deps evs deps)
+    let evx = Evarutil.undefined_evars_of_term evm x
+    and evy = Evarutil.undefined_evars_of_term evm y
+    in merge_deps (Intset.union evx evy) deps)
     cstrs deps
 
 let evar_dependencies evm =
   Evd.fold_undefined
     (fun ev evi acc ->
-      merge_deps (Intset.add ev (evars_of_evi evi evm)) acc)
+      merge_deps
+	(Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi)) acc)
     evm []
 
 (** [split_evars] returns groups of undefined evars according to dependencies *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 9e017bbd8f..171d77dd28 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -916,7 +916,7 @@ let apply_strategy (s : strategy) env sigma concl cstr evars =
 let split_evars_once sigma evd =
   Evd.fold_undefined (fun ev evi deps ->
     if Intset.mem ev deps then
-      Intset.union (Class_tactics.evars_of_evi evi evd) deps
+      Intset.union (Evarutil.undefined_evars_of_evar_info evd evi) deps
     else deps) evd sigma
 
 let existentials_of_evd evd =