huge commit regarding the grafite_status:

[helm.git] / helm / software / components / tactics / closeCoercionGraph.ml

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 2c67c95ee2a333154b80bce2ac3cc3760b783548..64df14a4243b3f67ef66daa81a26a369ad9a96bb 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -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