]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicUnifHint.ml
Good:
[helm.git] / helm / software / components / ng_refiner / nCicUnifHint.ml
index 6d80fe6ca46eb2d36eec7f61112dea7e94ecdeda..d166b19360fa391fd0a4febc334fe7f28bdaded5 100644 (file)
@@ -29,7 +29,9 @@ class status =
   val db = DB.empty
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
-  method set_unifhint_status (o : status) = {< db = o#uhint_db >}
+  method set_unifhint_status
+   : 'status. < uhint_db : db; .. > as 'status -> 'self
+   = fun o -> {< db = o#uhint_db >}
  end
 
 let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;