diff options
| author | Gaëtan Gilbert | 2019-07-02 15:31:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-02 15:31:21 +0200 |
| commit | 0cc7e942cd04f7fd28336045e43345b47a48b7a5 (patch) | |
| tree | ea174d1839f0f92bdfe11713bce88f522c10b580 /pretyping | |
| parent | 89b3d677b05b38d4708ffd756f15695c67d0cd6a (diff) | |
| parent | a4dcca3c2e08059848bde1c47c2aa76d78a9555d (diff) | |
Merge PR #10336: Improve the ambiguous paths warning to indicate which path is ambiguous with new one
Reviewed-by: SkySkimmer
Diffstat (limited to 'pretyping')
| -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 |