aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r--interp/coqlib.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5ac718e3b..b309f26cd 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -87,7 +87,7 @@ let check_required_library d =
*)
(* or failing ...*)
errorlabstrm "Coqlib.check_required_library"
- (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
+ (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
(************************************************************************)
(* Specific Coq objects *)