From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 18:48:37 +0000 (+0000)
Subject: Refinement of a Cast was bugged.
X-Git-Tag: V_0_7_2_3~110
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a71e7bb255a56ab53415da1e16dd289ea08353ea;p=helm.git

Refinement of a Cast was bugged.
---

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