diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 98414bf53..8a1186086 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -182,7 +182,7 @@ let compile verbosely f = let m = Names.id_of_string s in let _,longf = find_file_in_path (Library.get_load_path ()) (f^".v") in let ldir0 = Library.find_logical_path (Filename.dirname longf) in - let ldir = Names.extend_dirpath ldir0 m in + let ldir = Nameops.extend_dirpath ldir0 m in Lib.start_module ldir; load_vernac verbosely longf; let mid = Lib.end_module m in |