diff options
| author | letouzey | 2013-02-18 13:57:09 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-18 13:57:09 +0000 |
| commit | 648c594489f8d0ffdde9596b87f5c1ff6ccef612 (patch) | |
| tree | 8fef1eb15cad0a445ba9a07fe9f0f4c06febe727 /printing | |
| parent | 5d777a578b2973f57dffa9ca38d76bfda0551498 (diff) | |
Minor code cleanups, especially take advantage of Dir_path.is_empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | printing/printmod.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3a5cb784e6..0264f67fa8 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 -> diff --git a/printing/printmod.ml b/printing/printmod.ml index 5980dae0cd..c9341eeadb 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -208,7 +208,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with let rec printable_body dir = let dir = pop_dirpath dir in - dir = Dir_path.empty || + Dir_path.is_empty dir || try match Nametab.locate_dir (qualid_of_dirpath dir) with DirOpenModtype _ -> false |