diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml index 27c5056a7f..1acc8fd8fd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -138,7 +138,7 @@ let make_kn id = let mp = current_mp () in Names.KerName.make mp (Names.Label.of_id id) -let make_oname id = Libnames.make_oname !lib_state.path_prefix id +let make_oname id = Libobject.make_oname !lib_state.path_prefix id let recalc_path_prefix () = let rec recalc = function |