diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index ac89dfd74754e..ef54fb7ac8f22 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -30,29 +30,6 @@ type cl_typ =
   | CL_IND of inductive
   | CL_PROJ of Projection.Repr.t
 
-type cl_info_typ = {
-  cl_param : int
-}
-
-type coe_typ = GlobRef.t
-
-module CoeTypMap = GlobRef.Map_env
-
-type coe_info_typ = {
-  coe_value : GlobRef.t;
-  coe_local : bool;
-  coe_is_identity : bool;
-  coe_is_projection : Projection.Repr.t option;
-  coe_param : int;
-}
-
-let coe_info_typ_equal c1 c2 =
-  GlobRef.equal c1.coe_value c2.coe_value &&
-    c1.coe_local == c2.coe_local &&
-    c1.coe_is_identity == c2.coe_is_identity &&
-    c1.coe_is_projection == c2.coe_is_projection &&
-    Int.equal c1.coe_param c2.coe_param
-
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
   | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
@@ -60,14 +37,34 @@ let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
   | _ -> pervasives_compare t1 t2 (** OK *)
 
+let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
+
 module ClTyp = struct
   type t = cl_typ
   let compare = cl_typ_ord
 end
 
+module ClTypSet = Set.Make(ClTyp)
 module ClTypMap = Map.Make(ClTyp)
 
-let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
+type cl_info_typ = {
+  cl_param : int;
+  cl_reachable_from : ClTypSet.t;
+  cl_reachable_to : ClTypSet.t;
+  cl_repr : cl_typ;
+}
+
+type coe_typ = GlobRef.t
+
+module CoeTypMap = GlobRef.Map_env
+
+type coe_info_typ = {
+  coe_value : GlobRef.t;
+  coe_local : bool;
+  coe_is_identity : bool;
+  coe_is_projection : Projection.Repr.t option;
+  coe_param : int;
+}
 
 type inheritance_path = coe_info_typ list
 
@@ -85,10 +82,11 @@ sig
   type 'a t
   val empty : 'a t
   val mem : cl_typ -> 'a t -> bool
-  val map : Index.t -> 'a t -> cl_typ * 'a
-  val revmap : cl_typ -> 'a t -> Index.t * 'a
+  val find : Index.t -> 'a t -> cl_typ * 'a
+  val revfind : cl_typ -> 'a t -> Index.t * 'a
   val add : cl_typ -> 'a -> 'a t -> 'a t
   val dom : 'a t -> cl_typ list
+  val mapi : (Index.t -> cl_typ -> 'a -> 'b) -> 'a t -> 'b t
 end
 =
 struct
@@ -98,18 +96,28 @@ struct
   type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
   let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
   let mem y b = ClTypMap.mem y b.inv
-  let map x b = Int.Map.find x b.v
-  let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
+  let find x b = Int.Map.find x b.v
+  let revfind y b =
+    let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
   let add x y b =
     { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
   let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
+  let mapi f b = { v = Int.Map.mapi (fun i (cl, x) -> (cl, f i cl x)) b.v;
+                   s = b.s; inv = b.inv }
 end
 
 type cl_index = Bijint.Index.t
 
 let init_class_tab =
   let open Bijint in
-  add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
+  let cl_info params cl =
+    let cl_singleton = ClTypSet.singleton cl in
+    { cl_param = params;
+      cl_reachable_from = cl_singleton;
+      cl_reachable_to = cl_singleton;
+      cl_repr = cl }
+  in
+  add CL_FUN (cl_info 0 CL_FUN) (add CL_SORT (cl_info 0 CL_SORT) empty)
 
 let class_tab =
   Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t)
@@ -133,8 +141,7 @@ let inheritance_graph =
 (* ajout de nouveaux "objets" *)
 
 let add_new_class cl s =
-  if not (Bijint.mem cl !class_tab) then
-    class_tab := Bijint.add cl s !class_tab
+  class_tab := Bijint.add cl s !class_tab
 
 let add_new_coercion coe s =
   coercion_tab := CoeTypMap.add coe s !coercion_tab
@@ -144,13 +151,13 @@ let add_new_path x y =
 
 (* class_info : cl_typ -> int * cl_info_typ *)
 
-let class_info cl = Bijint.revmap cl !class_tab
+let class_info cl = Bijint.revfind cl !class_tab
 
 let class_exists cl = Bijint.mem cl !class_tab
 
 (* class_info_from_index : int -> cl_typ * cl_info_typ *)
 
-let class_info_from_index i = Bijint.map i !class_tab
+let class_info_from_index i = Bijint.find i !class_tab
 
 let cl_fun_index = fst(class_info CL_FUN)
 
@@ -328,31 +335,39 @@ let different_class_params env i =
       | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
       | _ -> false
 
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph env sigma (ic, cls, clt) =
+  let source, source_info = class_info cls in
+  let target, target_info = class_info clt in
   let old_inheritance_graph = !inheritance_graph in
-  let ambig_paths =
-    (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in
+  let ambig_paths :
+    ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref =
+    ref []
+  in
+  let check_coherence (i, j as ij) p q =
+    let cli, i_info = class_info_from_index i in
+    let clj, j_info = class_info_from_index j in
+    let between_ij =
+      ClTypSet.inter i_info.cl_reachable_from j_info.cl_reachable_to in
+    if cl_typ_eq cli i_info.cl_repr &&
+       cl_typ_eq clj j_info.cl_repr &&
+       ClTypSet.is_empty
+         (ClTypSet.diff (ClTypSet.inter between_ij source_info.cl_reachable_to)
+            i_info.cl_reachable_to) &&
+       ClTypSet.is_empty
+         (ClTypSet.diff
+            (ClTypSet.inter between_ij target_info.cl_reachable_from)
+            j_info.cl_reachable_from) &&
+       not (compare_path env sigma i p q)
+    then
+      ambig_paths := (ij, p, q) :: !ambig_paths
+  in
   let try_add_new_path (i,j as ij) p =
-    (* If p is a cycle, we check whether p is definitionally an identity
-       function or not. If it is not, we report p as an ambiguous inheritance
-       path. *)
-    if Bijint.Index.equal i j && not (compare_path env sigma i p []) then
-      ambig_paths := (ij,p,[])::!ambig_paths;
+    if Bijint.Index.equal i j then check_coherence ij p [];
     if not (Bijint.Index.equal i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
-        (* p has the same source and target classes as an existing path q. We
-           report them as ambiguous inheritance paths if
-           1. p and q have no common element, and
-           2. p and q are not convertible.
-           If 1 does not hold, say p = p1 @ [c] @ p2 and q = q1 @ [c] @ q2,
-           convertibility of p1 and q1, also, p2 and q2 should be checked; thus,
-           checking the ambiguity of p and q is redundant with them. *)
-        if not (List.exists (fun c -> List.exists (coe_info_typ_equal c) q) p ||
-                compare_path env sigma i p q) then
-          ambig_paths := (ij,p,q)::!ambig_paths;
-        false
-      | exception Not_found -> (add_new_path ij p; true)
+        (if not (Bijint.Index.equal i j) then check_coherence ij p q); false
+      | exception Not_found -> add_new_path ij p; true
     else
       false
   in
@@ -375,6 +390,27 @@ let add_coercion_in_graph env sigma (ic,source,target) =
          end)
       old_inheritance_graph
   end;
+  class_tab := Bijint.mapi (fun k clk k_info ->
+      let reachable_k_source = ClTypSet.mem clk source_info.cl_reachable_to in
+      let reachable_target_k = ClTypSet.mem clk target_info.cl_reachable_from in
+      { cl_param = k_info.cl_param;
+        cl_reachable_from =
+          if reachable_k_source then
+            ClTypSet.union
+              k_info.cl_reachable_from target_info.cl_reachable_from
+          else
+            k_info.cl_reachable_from;
+        cl_reachable_to =
+          if reachable_target_k then
+            ClTypSet.union k_info.cl_reachable_to source_info.cl_reachable_to
+          else
+            k_info.cl_reachable_to;
+        cl_repr =
+          if reachable_k_source && reachable_target_k then
+            target_info.cl_repr
+          else
+            k_info.cl_repr
+      }) !class_tab;
   match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
 
 type coercion = {
@@ -419,13 +455,17 @@ let class_params env sigma = function
 (* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
 let add_class env sigma cl =
-  add_new_class cl { cl_param = class_params env sigma cl }
+  if not (class_exists cl) then
+    let cl_singleton = ClTypSet.singleton cl in
+    add_new_class cl {
+      cl_param = class_params env sigma cl;
+      cl_reachable_from = cl_singleton;
+      cl_reachable_to = cl_singleton;
+      cl_repr = cl }
 
 let declare_coercion env sigma c =
   let () = add_class env sigma c.coercion_source in
   let () = add_class env sigma c.coercion_target in
-  let is, _ = class_info c.coercion_source in
-  let it, _ = class_info c.coercion_target in
   let xf =
     { coe_value = c.coercion_type;
       coe_local = c.coercion_local;
@@ -434,7 +474,7 @@ let declare_coercion env sigma c =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph env sigma (xf,is,it)
+  add_coercion_in_graph env sigma (xf, c.coercion_source, c.coercion_target)
 
 (* For printing purpose *)
 let pr_cl_index = Bijint.Index.print
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 073500b155e72..4c9c91d74c46f 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -31,9 +31,21 @@ val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
 (** Comparison of [cl_typ] *)
 val cl_typ_ord : cl_typ -> cl_typ -> int
 
+module ClTyp : Map.OrderedType with type t = cl_typ
+
+module ClTypSet : Set.S with type t = Set.Make(ClTyp).t
+
 (** This is the type of infos for declared classes *)
 type cl_info_typ = {
-  cl_param : int }
+  (* The number of parameters of the coercion class. *)
+  cl_param : int;
+  (* The sets of coercion classes respectively reachable from and to the
+     coercion class. *)
+  cl_reachable_from : ClTypSet.t;
+  cl_reachable_to : ClTypSet.t;
+  (* The representative class of the strongly connected component. *)
+  cl_repr : cl_typ;
+}
 
 (** This is the type of coercion kinds *)
 type coe_typ = GlobRef.t