X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=a4b10296f2f5f960d7074285abebcc34bccb3cbd;hb=33d0fc706f337453ceb6967dd4fcdc5fe55e65de;hp=f2467605f085731d456816feb325ca2e30e4b56a;hpb=10634c47be2ece4c088a1a1c1be5163952bf1c42;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index f2467605f..a4b10296f 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -71,6 +71,9 @@ let db () =
     (DB.empty,DB.empty) (CoercDb.to_list ())
 ;;
 
+let empty_db = (DB.empty,DB.empty) ;;
+
+
 let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
   match infty, expty with
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),