X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=a62238cfbc7aade664f85422222cfde19365b4dd;hb=738ff6e752f9e5facba4e92bdb64453062f52c7d;hp=9db93f0e1054cf6d23919d0b04a6bea78bb48cc3;hpb=e48acbc0d00717ce8f12412673ece4e4ee0e9642;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 9db93f0e1..a62238cfb 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -107,7 +107,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context =
   let res =
    match t with
     | C.Meta (i,(s,C.Ctx l)) ->
-       let l1 = U.sharing_map (aux (k-s)) l in
+       let l1 = HExtlib.sharing_map (aux (k-s)) l in
        if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
     | C.Meta _ -> t
     | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no)))