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 3a5cb784e..0264f67fa 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 = Dir_path.empty then + if Dir_path.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 (Dir_path.repr dir) <> [] then raise Not_found; + if not (Dir_path.is_empty dir) then raise Not_found; let (_,c,typ) = Global.lookup_named str in (print_named_decl (str,c,typ)) with Not_found -> |