X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.ml;h=6c253df9f73c9274ec1087b122415f9312374962;hb=4f1bd2790a4448a8ebfbe67eb8baa481c124745c;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..6c253df9f 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -25,7 +25,7 @@
 
 (* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *)
 
-let debug = false
+let debug = false 
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* given the new coercion uri from src to tgt returns the list 
@@ -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)
@@ -202,8 +207,10 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   let spline_len = saturations_for_c1 + saturations_for_c2 in
   let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
+  let old_insert_coercions = !CicRefine.insert_coercions in
   let c, metasenv, univ = 
     try
+      CicRefine.insert_coercions := false;
       let term, ty, metasenv, ugraph = 
         CicRefine.type_of_aux' metasenv context c univ
       in
@@ -246,11 +253,16 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       in
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
       debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+      CicRefine.insert_coercions := old_insert_coercions;
       term, metasenv, ugraph
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
+        CicRefine.insert_coercions := old_insert_coercions;
         raise UnableToCompose
+    | exn ->
+        CicRefine.insert_coercions := old_insert_coercions;
+        raise exn
   in  
   c, metasenv, univ 
 ;;