Test fixed.

[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 148450f5d17f1375b275186f3c08d807d0780a6b..f216b3c5c03429324561f49e8a89e770246063e1 100644 (file)
--- 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")