diff options
| author | Kazuhiko Sakaguchi | 2019-06-07 13:01:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-02 09:03:07 +0200 |
| commit | a4dcca3c2e08059848bde1c47c2aa76d78a9555d (patch) | |
| tree | 9e477686c491fd570d17cdfcbca87e4a51c58e7c /pretyping/classops.ml | |
| parent | 47389d31c0aa6fafa1c696b1e6f06059751a8217 (diff) | |
Improve the ambiguous paths warning to indicate which path is ambiguous with new one
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index f5fffc4c1c..afb546b2d2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -313,7 +313,9 @@ let compare_path p q = !path_comparator p q let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" - (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l) + (fun l -> prlist_with_sep fnl (fun (c,p,q) -> + str"New coercion path " ++ print_path (c,p) ++ + str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -330,13 +332,13 @@ let different_class_params env i = let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = - (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in + (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in let try_add_new_path (i,j as ij) p = if not (Bijint.Index.equal i j) || different_class_params env i then match lookup_path_between_class ij with | q -> if not (compare_path env sigma p q) then - ambig_paths := (ij,p)::!ambig_paths; + ambig_paths := (ij,p,q)::!ambig_paths; false | exception Not_found -> (add_new_path ij p; true) else |