From df53bf1e053026628822766f79aef9c050775949 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 4 Sep 2014 16:11:33 +0200 Subject: Fix: shelve_unifiable did not work modulo evar instantiation. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Irony… --- proofs/goal.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/goal.ml') diff --git a/proofs/goal.ml b/proofs/goal.ml index 1ada11745..6cdd315f8 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -99,14 +99,14 @@ let equal evars1 gl1 evars2 gl2 = the hypotheses, the conclusion or the body of the evar_info [evi]. Note: since we want to use it on goals, the body is actually supposed to be empty. *) -let contained_in_info e evi = - Evar.Set.mem e (Evarutil.evars_of_evar_info evi) +let contained_in_info sigma e evi = + Evar.Set.mem e (Evarutil.(evars_of_evar_info (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]. *) let depends_on sigma src tgt = let evi = Evd.find sigma tgt.content in - contained_in_info src.content evi + contained_in_info sigma src.content evi (* [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the -- cgit v1.2.3