diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
commit | 4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch) | |
tree | aefad2e3de35f75c46729f9310d33b56d3821961 /interp/coqlib.ml | |
parent | 64fa31c7ee53e79b112507fb2eea27dc7648328d (diff) | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r-- | interp/coqlib.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 02504c92..5ac718e3 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s = match these with | [x] -> x | [] -> - anomaly ~label:locstr (str ("cannot find "^s^ - " in module"^(if List.length dirs > 1 then "s " else " ")) ++ + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) | l -> anomaly ~label:locstr - (str ("ambiguous name "^s^" can represent ") ++ + (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) let gen_constant_in_modules locstr dirs s = @@ -86,7 +86,8 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(DirPath.to_string dir)^" has to be required first.") + errorlabstrm "Coqlib.check_required_library" + (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) |