X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=0074b291668f9690936b5571ccc39aa7e0bb5d3e;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=e17769ec98e2be2d0da4148490597dc26577581f;hpb=179cb3108e88369d855ba0088084be285fb19fdc;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index e17769ec9..0074b2916 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,40 +25,35 @@
 
 exception BaseUriNotSetYet
 
-type tactic = 
- (CicNotationPt.term, CicNotationPt.term, 
-  CicNotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic
-
-type lazy_tactic = 
-  (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
-    GrafiteAst.tactic
-
-val disambiguate_command: 
- LexiconEngine.status as 'status ->
- ?baseuri:string ->
- Cic.metasenv ->
- ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
-  'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+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 -> 
- (#NEstatus.status as 'status) ->
+ (#status as 'status) ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
+ NotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
- #NEstatus.status as 'status ->
+ #status as 'status ->
  ?baseuri:string ->
- (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+ (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
   'status * NCic.obj
 
 type pattern = 
-  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  NotationPt.term Disambiguate.disambiguator_input option * 
   (string * NCic.term) list * NCic.term option
 
 val disambiguate_npattern:
   GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
-    
-