diff options
| author | Pierre Boutillier | 2014-04-02 11:18:13 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-04-02 11:23:25 +0200 |
| commit | f963cf312d5a8ebb84af92489be5efd49fe6f434 (patch) | |
| tree | ffba990f8b32e55087acf1c57438c9bdb12602e2 | |
| parent | 502e61ec1ac488dd430ce6654c7a6947c6f7d1c3 (diff) | |
Better error message when found more than once object of name ...
| -rw-r--r-- | interp/coqlib.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index bf5b7db417..bf5d225b2c 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -58,10 +58,12 @@ let gen_constant_in_modules locstr dirs s = " in module"^(if List.length dirs > 1 then "s " else " ")) ++ prlist_with_sep pr_comma pr_dirpath dirs) | l -> - anomaly ~label:locstr - (str ("found more than once object of name "^s^ - " in module"^(if List.length dirs > 1 then "s " else " ")) ++ - prlist_with_sep pr_comma pr_dirpath dirs) + anomaly ~label:locstr + (str ("ambiguous name "^s^" 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 " ")) ++ + prlist_with_sep pr_comma pr_dirpath dirs) (* For tactics/commands requiring vernacular libraries *) |