aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/coqlib.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5fe0329f6b..ca3347dbbf 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -70,7 +70,7 @@ let check_required_library d =
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
- error ("Library "^(list_last d)^" has to be required first")
+ error ("Library "^(string_of_dirpath dir)^" has to be required first")
(************************************************************************)
(* Specific Coq objects *)