diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index a2f22b2e..dd74e192 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -7,13 +7,13 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names (**********************************************) -let pr_dirpath sl = (str (DirPath.to_string sl)) +let pr_dirpath sl = str (DirPath.to_string sl) (*s Operations on dirpaths *) @@ -197,7 +197,7 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> str (Id.to_string id) + | Ident (_,id) -> Id.print id let loc_of_reference = function | Qualid (loc,qid) -> loc |