diff options
Diffstat (limited to 'library/libobject.ml')
| -rw-r--r-- | library/libobject.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index 43934304c2..c153e9a09a 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Libnames open Pp module Dyn = Dyn.Make () @@ -18,10 +17,6 @@ type 'a substitutivity = type object_name = Libnames.full_path * Names.KerName.t -(* let make_oname (dirpath,(mp,dir)) id = *) -let make_oname { obj_dir; obj_mp } id = - Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id)) - type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; |