Refinement of a Cast was bugged.

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 9b9b02f7bf633ed160ea9eef4a99542f5529d7bd..e4532d913bf77d69027eda8420bb9e65cdd1c7ca 100644 (file)
--- 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