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

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 2cff9c608..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 
@@ -207,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
@@ -251,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 
 ;;