From: Claudio Sacerdoti Coen Date: Wed, 5 Sep 2007 10:07:39 +0000 (+0000) Subject: coercions are propagated under Fix (but not mutually recursive Fixes) X-Git-Tag: make_still_working~6075 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=870d26e5fbcb3159234e0eb06956cf295f72fedc;p=helm.git coercions are propagated under Fix (but not mutually recursive Fixes) --- diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 9ccf2b2ff..4c825c8a7 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1359,6 +1359,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il and coerce_to_something allow_coercions localization_tbl t infty expty subst metasenv context ugraph = + let module CS = CicSubstitution in let coerce_atom_to_something t infty expty subst metasenv context ugraph = let coer = CoercGraph.look_for_coercion metasenv subst context infty expty @@ -1412,9 +1413,26 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let clean t s c = whd c (CicMetaSubst.apply_subst s t) in let infty = clean infty subst context in let expty = clean expty subst context in - match infty, expty with - | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> - let module CS = CicSubstitution in + match infty, expty, t with + | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) -> + (match fl with + [name,i,_(* infty *),bo] -> + let context_bo = + Some (Cic.Name name,Cic.Decl expty)::context in + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux (Cic.Rel 1) expty infty subst + metasenv context_bo ugraph in + let bo = + CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo) + in + let (bo,_), subst, metasenv, ugraph = + coerce_to_something_aux bo infty expty subst + metasenv context_bo ugraph + in + (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph + | _ -> assert false (* not implemented yet *) + ) + | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> let name_con = Cic.Name "name_con" in let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in (* contravariant part: the argument of f:src->ty *)