huge commit regarding the grafite_status:

[helm.git] / helm / software / components / ng_refiner / nCicUnifHint.ml

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index b7d2b67d7642c87e5a30bed87eead2d74a7fd85f..9bd934c3b05ba86927634e925555a7bb84aba0a8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -137,7 +137,7 @@ let db () =
           if List.length l > 1 then 
            combine mk_hint l
           else [])
-      [] (CoercDb.to_list ())
+      [] (CoercDb.to_list (CoercDb.dump ()))
   in
   List.fold_left 
     (fun db -> function