little bug in coercion generation found. it use to create more coercions that expecte...

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 2cff9c608b19816edc3d571beb92431203c1b63c..6c253df9f73c9274ec1087b122415f9312374962 100644 (file)
--- a/components/tactics/closeCoercionGraph.ml
+++ b/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 
 ;;