Objects are now used to represent also the tactic status.

[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..6d80fe6ca46eb2d36eec7f61112dea7e94ecdeda 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -29,6 +29,7 @@ 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 >}
  end
 
 let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;