diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 0264f67fa..732903af9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -331,7 +331,7 @@ let print_located_qualid ref = match List.map expand (N.locate_extended_all qid) with | [] -> let (dir,id) = repr_qualid qid in - if Dir_path.is_empty dir then + if DirPath.is_empty dir then str "No object of basename " ++ pr_id id else str "No object of suffix " ++ pr_qualid qid @@ -634,7 +634,7 @@ let print_any_name = function | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in - if not (Dir_path.is_empty dir) then raise Not_found; + if not (DirPath.is_empty dir) then raise Not_found; let (_,c,typ) = Global.lookup_named str in (print_named_decl (str,c,typ)) with Not_found -> |