diff options
| author | msozeau | 2009-06-18 17:59:35 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-18 17:59:35 +0000 |
| commit | 9346d0b22d34a48b16f46c663064808063afb4a2 (patch) | |
| tree | 73d53b1d794edb930c0d8302538bdb1cf8c54d02 /tactics | |
| 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')
| -rw-r--r-- | tactics/class_tactics.ml4 | 12 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 8 |
2 files changed, 10 insertions, 10 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 9146d02c5c..1163547bf9 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) -> diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 7260f1fd7e..32155f0543 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -742,16 +742,10 @@ let apply_strategy (s : strategy) env sigma concl cstr evars = evars := res.rew_evars; Some (Some (res.rew_prf, (res.rew_car, res.rew_rel, res.rew_from, res.rew_to))) -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_once sigma evd = Evd.fold (fun ev evi deps -> if Intset.mem ev deps then - Intset.union (evars_of_evi evi) deps + Intset.union (Class_tactics.evars_of_evi evi) deps else deps) evd sigma let existentials_of_evd evd = |