X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.ml;h=2cff9c608b19816edc3d571beb92431203c1b63c;hb=4f2e7eacea9e8b3089a575d7bf529fd5e70e8453;hp=d9dc679b32c35c85cafd5b25b68c66f45df554e3;hpb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;p=helm.git

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index d9dc679b3..2cff9c608 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -52,15 +52,20 @@ let get_closure_coercions src tgt uri coercions =
           coercions 
       in
         (HExtlib.flatten_map 
-          (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+          (fun (_,t,ul) -> 
+             if CoercDb.eq_carr ~exact:true src t then [] else
+             List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
         (HExtlib.flatten_map 
-          (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+          (fun (s,_,ul) -> 
+             if CoercDb.eq_carr ~exact:true s tgt then [] else
+             List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
         (HExtlib.flatten_map 
           (fun (s,_,u1l) ->
             HExtlib.flatten_map 
               (fun (_,t,u2l) ->
                 HExtlib.flatten_map
                   (fun u1 ->
+                    if CoercDb.eq_carr ~exact:true s t then [] else
                     List.map 
                       (fun u2 -> (s,[u1;uri;u2],t)) 
                       u2l)