From c97a507293db3d4627250ecc433d71f48b0df130 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 3 Feb 2011 20:22:33 +0000
Subject: 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
---
 tactics/class_tactics.ml4 | 16 +++++-----------
 tactics/rewrite.ml4       |  2 +-
 2 files changed, 6 insertions(+), 12 deletions(-)

(limited to 'tactics')

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 =
-- 
cgit v1.2.3