From ae0f6455129a66c243b7e0fe858aa779f8b956c2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 29 Sep 2014 18:41:27 +0200 Subject: 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. --- proofs/goal.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/goal.ml') 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]. *) -- cgit v1.2.3