diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ef0fb8ea6..8652a4146 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -679,6 +679,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let filter1 = evar_filter evi1 in let src = subterm_source evk1 evi1.evar_source in let ids1 = List.map get_id (named_context_of_val sign1) in + let avoid = Context.Named.to_vars (named_context_of_val sign1) in let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in let open Context.Rel.Declaration in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = @@ -700,9 +701,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), - push_rel d env,evd,id::avoid)) + push_rel d env,evd,Id.Set.add id avoid)) rel_sign - (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) + (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in |