From b103459011e65c09d481bdaee5fd7ce7638fb139 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 25 Sep 2008 20:16:23 +0000
Subject: Partial fix for bug #1948: recompute order of dependencies between
 evars at the end of unification as later evars can refer to previous ones.
 This removes the assumption that evars are already ordered in eterm's code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11419 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 115e47ae18..e9bd15b119 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -61,14 +61,6 @@ let init_setoid () =
 
 (** Typeclasses instance search tactic / eauto *)
 
-let evars_of_term init c = 
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) -> Intset.add n acc
-    | _ -> fold_constr evrec acc c
-  in 
-    evrec init c
-
 let intersects s t =
   Intset.exists (fun el -> Intset.mem el t) s
 
@@ -183,14 +175,14 @@ let rec catchable = function
   | e -> Logic.catchable_exception e
 
 let is_dep gl gls =
-  let evs = evars_of_term Intset.empty gl.evar_concl in
+  let evs = Evarutil.evars_of_term gl.evar_concl in
     if evs = Intset.empty then false
     else
       List.fold_left
 	(fun b gl -> 
 	  if b then b 
 	  else
-	    let evs' = evars_of_term Intset.empty gl.evar_concl in
+	    let evs' = Evarutil.evars_of_term gl.evar_concl in
 	      intersects evs evs')
 	false gls
 	
@@ -455,7 +447,7 @@ let rec merge_deps deps = function
 	
 let split_evars evm =
   Evd.fold (fun ev evi acc ->
-    let deps = evars_of_term (Intset.singleton ev) evi.evar_concl in
+    let deps = Intset.union (Intset.singleton ev) (Evarutil.evars_of_term evi.evar_concl) in
       merge_deps deps acc)
     evm []
 
-- 
cgit v1.2.3