removed debug code

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

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index f2467605f085731d456816feb325ca2e30e4b56a..a4b10296f2f5f960d7074285abebcc34bccb3cbd 100644 (file)
--- 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 _::_)),