X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=7590699f9412cab82aede8649e3378be45610417;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=439a817d3f5f127318dfc789e689fb6174edbf87;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 439a817d3..7590699f9 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -26,8 +26,8 @@
 exception BaseUriNotSetYet
 
 type tactic = 
- (CicNotationPt.term, CicNotationPt.term, 
-  CicNotationPt.term GrafiteAst.reduction, string) 
+ (NotationPt.term, NotationPt.term, 
+  NotationPt.term GrafiteAst.reduction, string) 
    GrafiteAst.tactic
 
 type lazy_tactic = 
@@ -37,24 +37,24 @@ type lazy_tactic =
 val disambiguate_command: 
  LexiconEngine.status as 'status ->
  ?baseuri:string ->
- ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
+ ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
   'status * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_nterm :
  NCic.term option -> 
  (#NEstatus.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 ->
  ?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: