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 9ccf2b2ffd2b6be1306357d19c0d2a9361b5f3e1..4c825c8a7313ac8385d85d8610520a0a1e84ba6a 100644 (file)
--- 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 *)