diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-18 17:59:35 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-18 17:59:35 +0000 |
| commit | 9346d0b22d34a48b16f46c663064808063afb4a2 (patch) | |
| tree | 73d53b1d794edb930c0d8302538bdb1cf8c54d02 /tactics/class_tactics.ml4 | |
| parent | 918777908845fde7b6f8e3361f2ed145eb98886b (diff) | |
Fix "unsatisfiable constraints" error messages to include all the
necessary information. Fix implementation of [split_evars] and
use splitting more wisely as it has a big performance impact.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12196 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 9146d02c5..1163547bf 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -417,9 +417,15 @@ let rec merge_deps deps = function merge_deps (Intset.union deps hd) tl else hd :: merge_deps deps tl +let evars_of_evi evi = + Intset.union (Evarutil.evars_of_term evi.evar_concl) + (match evi.evar_body with + | Evar_defined b -> Evarutil.evars_of_term b + | Evar_empty -> Intset.empty) + let split_evars evm = Evd.fold (fun ev evi acc -> - let deps = Intset.union (Intset.singleton ev) (Evarutil.evars_of_term evi.evar_concl) in + let deps = Intset.union (Intset.singleton ev) (evars_of_evi evi) in merge_deps deps acc) evm [] @@ -430,7 +436,7 @@ let select_evars evs evm = let resolve_all_evars debug m env p oevd do_split fail = let oevm = oevd in - let split = if do_split then split_evars (Evd.undefined_evars oevd) else [Intset.empty] in + let split = if do_split then split_evars oevd else [Intset.empty] in let p = if do_split then fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi else fun _ -> p @@ -450,7 +456,7 @@ let resolve_all_evars debug m env p oevd do_split fail = match res with | None -> if fail then - (* Unable to satisfy the constraints. *) + (* Unable to satisfy the constraints. *) let evm = if do_split then select_evars comp evd else evd in let _, ev = Evd.fold (fun ev evi (b,acc) -> |