Fixed (yet another) nasty bug, in deep_eq this time

[helm.git] / helm / software / components / ng_refiner / nCicUnifHint.ml

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index ccccfca88742dfd48b1ef1a892229f70cd502e12..d166b19360fa391fd0a4febc334fe7f28bdaded5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -29,6 +29,9 @@ class status =
   val db = DB.empty
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
+  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");;