]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicCoercion.ml
ugly coerc db print
[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml
index 7d5d0101ad3de62287ad4197d6465a0efee51540..fd697265a2464e4c9255eb6f844fd796b2fe6bac 100644 (file)
@@ -31,6 +31,12 @@ type db = DB.t * DB.t
 
 let empty_db = DB.empty,DB.empty
 
+class type g_status =
+ object
+  inherit NCicUnifHint.g_status
+  method coerc_db: db
+ end
+
 class status =
  object
   inherit NCicUnifHint.status
@@ -38,9 +44,8 @@ class status =
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
   method set_coercion_status
-  : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> 
-          'self
-          = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
+   : 'status. #g_status as 'status -> 'self
+   = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
 let index_coercion status name c src tgt arity arg =