X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=e334861cbf9c0482f02e8e7401f6fb24e8b7f4c6;hb=90dd88139a78b4dd650d5c462ecf602bf4813cd4;hp=d2ad6a55f799015fc044550953dd18bf1d649887;hpb=20e70a2cdbafd0c720e1e6682e0497e6ed964439;p=helm.git

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index d2ad6a55f..e334861cb 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -186,7 +186,7 @@ let does_not_occur status ~subst context n nn t =
     | C.Rel m when m <= k || m > nn+k -> ()
     | C.Rel m ->
         (try match List.nth context (m-1-k) with
-          | _,C.Def (bo,_) -> aux (n-m) () bo
+          | _,C.Def (bo,_) -> aux 0 () (S.lift status (m-k) bo)
           | _ -> ()
          with Failure _ -> assert false)
     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
@@ -1131,7 +1131,7 @@ and get_relevance status ~metasenv ~subst context t args =
               | C.Sort C.Prop ->
                   false::(aux context new_ty tl)
               | C.Sort _
-                   | C.Meta _ -> true::(aux context new_ty tl)
+              | C.Meta _ -> true::(aux context new_ty tl)
               | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
                      "Prod: the type %s of the source of %s is not a sort" 
                       (status#ppterm ~subst ~metasenv ~context sort)