This commit patches the environment and the library so that their status is

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

diff --git a/matitaB/components/ng_refiner/nCicUnifHint.mli b/matitaB/components/ng_refiner/nCicUnifHint.mli
index 832e980e21f163c26208602009a473ff8fdc0808..fafc4a6f860752cd13d546ed5e80d7aacf296c38 100644 (file)
--- a/matitaB/components/ng_refiner/nCicUnifHint.mli
+++ b/matitaB/components/ng_refiner/nCicUnifHint.mli
@@ -21,9 +21,10 @@ class type g_status =
  end
 
 class virtual status :
+ string option ->
  object ('self)
   inherit g_status
-  inherit NCic.status
+  inherit NCicEnvironment.status
   method set_uhint_db: db -> 'self
   method set_unifhint_status: #g_status -> 'self
  end