diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-15 16:43:42 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-15 16:43:42 +0000 |
| commit | d536aeb0c465b62c708ba4c70fd31b82c24168a5 (patch) | |
| tree | d064289b76beb81b29f3173df6670d0a93847de5 /tactics/class_tactics.ml4 | |
| parent | ed39b35b780c1fac9eb110f303014683e6640c01 (diff) | |
Misc improvements about evar_map
- A Evd.defined_evars to keep only this part of the evar_map
- One Evd.fold less in Typeclasses.mark_unresolvables
- We check that only undefined evar_map could be set unresolvable
- A duplicated function in himsg.ml
TODO: some calls to Evd.fold(_undefined) would be faster if written
as Map.map or Map.mapi.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index bc415e78a..2f85668a7 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -54,17 +54,9 @@ let evars_to_goals p evm = let evi', goal = p evm ev evi in let gls' = if goal then (ev,Goal.V82.build ev) :: gls else gls in (gls', Evd.add evm' ev evi')) - evm ([], Evd.empty) + evm ([], Evd.defined_evars evm) in - if goals = [] then None - else - let goals = List.rev goals in - (** old defined evars of [evm] + new undefined ones of [evm'] *) - let evm' = - Evd.fold_undefined (fun ev evi evm -> Evd.add evm ev evi) evm' evm - in - let evm' = evars_reset_evd evm' evm in - Some (goals, evm') + if goals = [] then None else Some (List.rev goals, evm') (** Typeclasses instance search tactic / eauto *) |