X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=0168d2d7573493a91fc67891b43b71ee0e48270f;hb=3f551aa5900d5c756eb48cea751c032b3bcbcf37;hp=f55b1fed0e646de07d387aacfad9aae8bc60d11f;hpb=f386b970edc5798769c96e44f5c9ab30efa06605;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index f55b1fed0..0168d2d75 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -405,6 +405,37 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
+            let rec count_prods context ty =
+              match CicReduction.whd context ~subst:subst'' ty with
+              | Cic.Prod (n,s,t) -> 
+                 1 + count_prods (Some (n,Cic.Decl s)::context) t
+              | _ -> 0
+            in
+            let exp_prods = count_prods context ty' in
+            let inf_prods = count_prods context inferredty in
+            let te', inferredty, metasenv'', subst'', ugraph2 =
+               let rec aux t m s ug it = function
+                 | 0 -> t,it,m,s,ug
+                 | n ->
+                      match CicReduction.whd context ~subst:s it with
+                      | Cic.Prod (_,src,tgt) -> 
+                          let newmeta, metaty, s, m, ug =
+                            type_of_aux s m context (Cic.Implicit None) ug
+                          in
+                          let s,m,ug = 
+                            fo_unif_subst s context m metaty src ug
+                          in
+                          let t =
+                            match t with
+                            | Cic.Appl l -> Cic.Appl (l @ [newmeta])
+                            | _ -> Cic.Appl [t;newmeta]
+                          in
+                          aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
+                      | _ -> t,it,m,s,ug     
+               in
+                 aux te' metasenv'' subst'' ugraph2 inferredty
+                   (max 0 (inf_prods - exp_prods))
+            in
             let (te', ty'), subst''',metasenv''',ugraph3 =
               coerce_to_something true localization_tbl te' inferredty ty'
                 subst'' metasenv'' context ugraph2
@@ -1160,7 +1191,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
       | CoercGraph.SomeCoercion candidates -> 
          let selected =
            HExtlib.list_findopt
-             (function (metasenv,last,c) ->
+             (fun (metasenv,last,c) _ ->
                match c with 
                | c when not (CoercGraph.is_composite c) -> 
                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
@@ -1314,7 +1345,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 ugraph in
               match
                 HExtlib.list_findopt
-                 (fun (he,hetype,subst,metasenv,ugraph) ->
+                 (fun (he,hetype,subst,metasenv,ugraph) _ ->
                    (* {{{ *)debug_print (lazy ("Try fix: "^
                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
                    debug_print (lazy (" of type: "^