diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a4052ac82..4287db520 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -400,7 +400,7 @@ let print_located_module r = let dir = Nametab.full_name_module qid in msg_notice (str "Module " ++ pr_dirpath dir) with Not_found -> - if Dir_path.equal (fst (repr_qualid qid)) Dir_path.empty then + if Dir_path.is_empty (fst (repr_qualid qid)) then msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid) else msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid) |