Cic.term and Cic.obj unused!

[helm.git] / matita / components / ng_refiner / nCicCoercion.mli

diff --git a/matita/components/ng_refiner/nCicCoercion.mli b/matita/components/ng_refiner/nCicCoercion.mli
index 1094753cfb1ed5b3c942ceef1c2fc88d37a63d84..f2cd526822b1f5342bf95fd1a27b307934a18c6e 100644 (file)
--- a/matita/components/ng_refiner/nCicCoercion.mli
+++ b/matita/components/ng_refiner/nCicCoercion.mli
@@ -13,9 +13,6 @@
 
 type db
 
-val set_convert_term:
- (UriManager.uri -> Cic.term -> NCic.term * NCic.obj list) -> unit
-
 class type g_status =
  object
   inherit NCicUnifHint.g_status