From 62112e387e868923a13e07b0844cc8bf2b0a108b Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 26 Mar 2012 22:29:25 +0000 Subject: Unification: Fixing bug in materialize_evar (spotted by MathClasses). Also fixed apparent other bug in the presence of let-ins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15099 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarutil.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 00501a893..c509fe9da 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -822,12 +822,13 @@ let make_pure_subst evi args = * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds. *) -let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env - inst_in_sign = +let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env = let ty_t_in_env = Retyping.get_type_of env evd t_in_env in let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in let t_in_env = whd_evar evd t_in_env in let evd = define_fun env evd (destEvar evar_in_env) t_in_env in + let ids = List.map pi1 (named_context_of_val sign) in + let inst_in_sign = List.map mkVar (list_filter_with filter ids) in let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in (evd,whd_evar evd evar_in_sign) @@ -857,27 +858,26 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) -> - match b with - | None -> - let id = next_name_away na avoid in - let evd,t_in_sign = - define_evar_from_virtual_equation define_fun env evd t_in_env - sign filter inst_in_env inst_in_sign in - (push_named_context_val (id,None,t_in_sign) sign,true::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) + let id = next_name_away na avoid in + let evd,t_in_sign = + define_evar_from_virtual_equation define_fun env evd t_in_env + sign filter inst_in_env in + let evd,b_in_sign = match b with + | None -> evd,None | Some b -> - (sign,filter, - List.map (lift 1) inst_in_env, - List.map (lift 1) inst_in_sign, - push_rel d env,evd,avoid)) + let evd,b = define_evar_from_virtual_equation define_fun env evd b + sign filter inst_in_env in + evd,Some b in + (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::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)) rel_sign (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) in let evd,ev2ty_in_sign = define_evar_from_virtual_equation define_fun env evd ty_in_env - sign2 filter2 inst2_in_env inst2_in_sign in + sign2 filter2 inst2_in_env in let evd,ev2_in_sign = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in -- cgit v1.2.3