diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 15:59:28 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 15:59:28 +0200 |
| commit | f30269579b78d5bf65dcd5db70e341fe9598b274 (patch) | |
| tree | f5a05e9e0dedac688e9d71e3576a25a576fa8822 /tactics/class_tactics.ml | |
| parent | 4d858df22bb30d2efbef39a177c28c15c600c885 (diff) | |
| parent | 1517d56d3588eaa9097683bc56c987069f04592f (diff) | |
Merge PR #892: Improve do_split option of typeclass resolution
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6cb56d64f..6cc9d3d55 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1424,18 +1424,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 @@ -1520,7 +1522,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 |