Objects are now used to represent also the tactic status.

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

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index f7257d8f8472c03978429f8d34700abc88e65421..fa65d527766096d4e3991be4cc4808eea8c307ac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -17,6 +17,7 @@ class status :
  object ('self)
   method uhint_db: db
   method set_uhint_db: db -> 'self
+  method set_unifhint_status: status -> 'self
  end
 
 val index_hint: