X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=f216b3c5c03429324561f49e8a89e770246063e1;hb=67906d4803b6bb6740382d8cbd31d8c0e7322c7d;hp=148450f5d17f1375b275186f3c08d807d0780a6b;hpb=f951f6a1c14f33b624789bcf60e80d8307b461d3;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 148450f5d..f216b3c5c 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -174,7 +174,12 @@ and type_of_aux' metasenv context t ugraph =
 		 | Some (_,C.Def (_,Some ty)) -> 
                      t,S.lift n ty,subst,metasenv, ugraph
 		 | Some (_,C.Def (bo,None)) ->
-		     type_of_aux subst metasenv context (S.lift n bo) ugraph 
+                     let ty,ugraph =
+                      (* if it is in the context it must be already well-typed*)
+		      CicTypeChecker.type_of_aux' ~subst metasenv context
+                       (S.lift n bo) ugraph 
+                     in
+                      t,ty,subst,metasenv,ugraph
 		 | None -> raise (RefineFailure "Rel to hidden hypothesis")
              with
 		 _ -> raise (RefineFailure "Not a close term")