Multi-user matita: changed the status object to include a ``user'' method

[helm.git] / matitaB / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 0cadc45b77334950c04a9d37c64d14c3fb43eccb..30bd9b83497417ef9e3737827620de485e3b0ba2 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -51,9 +51,9 @@ class type g_status =
    method disambiguate_db: db
   end
 
-class virtual status =
+class virtual status uid =
  object (self)
-  inherit Interpretations.status
+  inherit Interpretations.status uid
   val disambiguate_db = initial_status
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}