X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.ml;h=64df14a4243b3f67ef66daa81a26a369ad9a96bb;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=07308b4077fddd603a1f3088e9240c6b2ca2eeb7;hpb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;p=helm.git

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 07308b407..64df14a42 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -199,7 +199,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
     let l_c2 = skip_appl (purge_lambdas term) in
     let l_c2_b,l_c2_a =
      try
-      HExtlib.split_nth "CCG 1" (c2_pis - sat2 - 1) l_c2
+      HExtlib.split_nth (c2_pis - sat2 - 1) l_c2
      with
       Failure _ -> assert false in
     let l_c1,l_c2_a =
@@ -476,7 +476,7 @@ let number_if_already_defined buri name l =
  *)
 let close_coercion_graph src tgt uri saturations baseuri =
   (* check if the coercion already exists *)
-  let coercions = CoercDb.to_list () in
+  let coercions = CoercDb.to_list (CoercDb.dump ()) in
   let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in
   debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
   let todo_list = filter_duplicates todo_list coercions in