diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-29 18:41:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-29 19:09:13 +0200 |
| commit | ae0f6455129a66c243b7e0fe858aa779f8b956c2 (patch) | |
| tree | 6ba5ed428c4eddfc1b8d2cce1000cb9fc46019e0 /tactics/class_tactics.ml | |
| parent | 5e5523f9e3211052f537cc90841fc295c67fc07f (diff) | |
Merging some functions from evarutil.ml/evd.ml.
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 35889462b..d9f90b02e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -157,7 +157,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = try let cl = Typeclasses.class_info (fst hdc) in if cl.cl_strict then - Evarutil.evars_of_term concl + Evd.evars_of_term concl else Evar.Set.empty with _ -> Evar.Set.empty in |