From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 26 Jul 2007 10:39:38 +0000 (+0000)
Subject: little bug in coercion generation found. it use to create more coercions that expecte... 
X-Git-Tag: 0.4.95@7852~275
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dfbd010fe5a46d049849913bc23000289893ea4f;p=helm.git

little bug in coercion generation found. it use to create more coercions that expected (luckily convertible).
---

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 2cff9c608..6c253df9f 100644
--- 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 
 ;;