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

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 9b9b02f7b..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