- oCic2NCic and nCic2OCic moved to ng_library

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

diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli
index 0f514eef69ba86ed9dd33c245852f9c37f0b6780..ff6b439974c12f5dfc7b0eea9942629da09d9b93 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.mli
+++ b/helm/software/components/ng_refiner/nCicCoercion.mli
@@ -13,6 +13,9 @@
 
 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