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 /proofs/goal.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 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index b0fccc42f..ce7f5959a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -101,7 +101,7 @@ let equal evars1 gl1 evars2 gl2 = [evi]. Note: since we want to use it on goals, the body is actually supposed to be empty. *) let contained_in_info sigma e evi = - Evar.Set.mem e (Evarutil.(evars_of_evar_info (nf_evar_info sigma evi))) + Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) (* [depends_on sigma src tgt] checks whether the goal [src] appears as an existential variable in the definition of the goal [tgt] in [sigma]. *) |