]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicUtils.mli
loc * lazy string -> (loc * string) lazy
[helm.git] / helm / software / components / ng_kernel / nCicUtils.mli
index 11eca58c02f6fa0b0ab91a3baf2a7afdb859b968..c87dd6638b72b4bfa7211fc83a6ec21b6004ee4c 100644 (file)
@@ -14,8 +14,6 @@
 exception Subst_not_found of int
 exception Meta_not_found of int
 
-val sharing_map: ('a -> 'a) -> 'a list -> 'a list
-
 val expand_local_context : NCic.lc_kind -> NCic.term list
 
 val lookup_subst: int ->  NCic.substitution -> NCic.subst_entry