]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/grafite_parser/grafiteDisambiguate.ml
- dependencies between statuses simplified
[helm.git] / matita / components / grafite_parser / grafiteDisambiguate.ml
index 58a241e3fdc782511125d882e823350d5f4449fb..7511e02aaad65670504ea7a23cd0902990da0148 100644 (file)
 class type g_status =
   object
    inherit LexiconTypes.g_status
-   inherit NCicCoercion.g_status
   end
 
 class status =
  object (self)
   inherit LexiconTypes.status
-  inherit NCicCoercion.status
   method set_grafite_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
+      = fun o -> (self#set_lexicon_engine_status o)
  end
 
 exception BaseUriNotSetYet