X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=e4532d913bf77d69027eda8420bb9e65cdd1c7ca;hb=118769957a508c21b72bd7b9d2dbf64f654fe21c;hp=a0dfb9f2889e2d7bb024a1e08b28c8d756616078;hpb=f0b23f17200a0b86a1f53cac172a333ddbd8181d;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a0dfb9f28..e4532d913 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -360,14 +360,11 @@ and type_of_aux' metasenv context t ugraph =
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
-              (try
                  let subst''',metasenv''',ugraph3 =
                    fo_unif_subst subst'' context metasenv'' 
-                     inferredty ty ugraph2
+                     inferredty ty' ugraph2
                  in
                    C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
-               with
-               | _ -> raise (RefineFailure (lazy "Cast")))
         | C.Prod (name,s,t) ->
             let carr t subst context = CicMetaSubst.apply_subst subst t in
             let coerce_to_sort 
@@ -480,7 +477,7 @@ and type_of_aux' metasenv context t ugraph =
                 ) tl ([],subst',metasenv',ugraph1)
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
-              eat_prods subst'' metasenv'' context 
+              eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
@@ -743,6 +740,22 @@ and type_of_aux' metasenv context t ugraph =
                         (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
+             let outtype,outtypety, subst, metasenv,ugraph4 =
+               type_of_aux subst metasenv context outtype ugraph4
+             in
+             let tlbody_and_type,subst,metasenv,ugraph4 =
+               List.fold_right
+                 (fun x (res,subst,metasenv,ugraph) ->
+                    let x',ty,subst',metasenv',ugraph1 =
+                      type_of_aux subst metasenv context x ugraph
+                    in
+                      (x', ty)::res,subst',metasenv',ugraph1
+                 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+             in
+             let _,_,subst,metasenv,ugraph4 =
+               eat_prods false subst metasenv context 
+                 outtypety tlbody_and_type ugraph4
+             in
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
@@ -1000,7 +1013,9 @@ and type_of_aux' metasenv context t ugraph =
                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
                 (CicPp.ppterm t2''))))
 
-  and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
+  and eat_prods 
+    allow_coercions subst metasenv context hetype tlbody_and_type ugraph 
+  =
     let rec mk_prod metasenv context =
       function
           [] ->
@@ -1067,7 +1082,7 @@ and type_of_aux' metasenv context t ugraph =
                          fo_unif_subst subst context metasenv hety s ugraph
                        in
                          hete,subst,metasenv,ugraph1
-                     with exn ->
+                     with exn when allow_coercions ->
                        (* we search a coercion from hety to s *)
                        let coer = 
                          let carr t subst context =