]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_refiner/nCicCoercion.mli
- cleanup
[helm.git] / matita / components / ng_refiner / nCicCoercion.mli
index 1094753cfb1ed5b3c942ceef1c2fc88d37a63d84..d85484a2a4d02959f2451bea524972c56b5fc152 100644 (file)
@@ -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
@@ -24,9 +21,8 @@ class type g_status =
 
 class status :
  object ('self)
-  inherit NCicUnifHint.status
   inherit g_status
-  method coerc_db: db
+  inherit NCicUnifHint.status
   method set_coerc_db: db -> 'self
   method set_coercion_status: #g_status -> 'self
  end