nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 9db93f0e1054cf6d23919d0b04a6bea78bb48cc3..a62238cfbc7aade664f85422222cfde19365b4dd 100644 (file)
--- 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)))