- dependencies between statuses simplified

[helm.git] / matita / components / grafite_parser / grafiteDisambiguate.mli

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 0074b291668f9690936b5571ccc39aa7e0bb5d3e..6caf5301f200f0f8c667ae5bf534dd5ae8e6c63f 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,28 +25,15 @@
 
 exception BaseUriNotSetYet
 
-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: #g_status -> 'self
- end
-
 val disambiguate_nterm :
  NCic.term option -> 
- (#status as 'status) ->
+ (#LexiconTypes.status as 'status) ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  NotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
- #status as 'status ->
+ #LexiconTypes.status as 'status ->
  ?baseuri:string ->
  (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
   'status * NCic.obj