aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-07-17 22:33:53 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2017-07-18 16:14:39 +0200
commit1517d56d3588eaa9097683bc56c987069f04592f (patch)
tree0cfe493b1cc294f2c467b4db5a0e5e8e7cd55dbc /tactics
parent0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff)
Improve do_split option of typeclass resolution
It used to compute the dependencies of all undefined evars of the evar_map, while only the dependencies of resolvable evars are necessary.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml14
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7a8595653..55df67c6e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1425,18 +1425,20 @@ let deps_of_constraints cstrs evm p =
Intpart.union_set (Evar.Set.union evx evy) p)
cstrs
-let evar_dependencies evm p =
+let evar_dependencies pred evm p =
Evd.fold_undefined
(fun ev evi _ ->
- let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
- in Intpart.union_set evars p)
+ if Typeclasses.is_resolvable evi && pred evm ev evi then
+ let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+ in Intpart.union_set evars p
+ else ())
evm ()
(** [split_evars] returns groups of undefined evars according to dependencies *)
-let split_evars evm =
+let split_evars pred evm =
let p = Intpart.create () in
- evar_dependencies evm p;
+ evar_dependencies pred evm p;
deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p;
Intpart.partition p
@@ -1521,7 +1523,7 @@ exception Unresolved
(** If [do_split] is [true], we try to separate the problem in
several components and then solve them separately *)
let resolve_all_evars debug depth unique env p oevd do_split fail =
- let split = if do_split then split_evars oevd else [Evar.Set.empty] in
+ let split = if do_split then split_evars p oevd else [Evar.Set.empty] in
let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
in
let rec docomp evd = function