diff options
| author | msozeau | 2008-09-25 20:16:23 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-25 20:16:23 +0000 |
| commit | b103459011e65c09d481bdaee5fd7ce7638fb139 (patch) | |
| tree | 7729ca2f988096f6fc50dde32d76534326051874 /tactics | |
| parent | f9cbb56333230d81338f1d223e2c08343a1095eb (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 14 |
1 files changed, 3 insertions, 11 deletions
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 [] |