Refiner substituted with the type-checker in a case that is known to be already

well-typed.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index df7eca08f398f35141d021091d254c0a7408ba88..f216b3c5c03429324561f49e8a89e770246063e1 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -174,8 +174,10 @@ 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)) ->
-                     let _,ty,subst,metasenv,ugraph =
-                     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")