X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.mli;h=25ac95ff47bffddbe9ee340f6d422c268205aff1;hb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;hp=d28708e3a533565276449683e61bc6be95ad308c;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli
index d28708e3a..25ac95ff4 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli
@@ -30,7 +30,7 @@ val disambiguate_term :
     DisambiguateTypes.input_or_locate_uri_type ->
     DisambiguateTypes.Environment.key ->
     'alias list) ->
-  CicNotationPt.term Disambiguate.disambiguator_input ->
+  NotationPt.term Disambiguate.disambiguator_input ->
   ((DisambiguateTypes.domain_item * 'alias) list *
    NCic.metasenv *                  
    NCic.substitution *
@@ -51,10 +51,10 @@ val disambiguate_obj :
     DisambiguateTypes.Environment.key ->
      'alias list) ->
   uri:NUri.uri ->
-  string * int * CicNotationPt.term CicNotationPt.obj ->
+  string * int * NotationPt.term NotationPt.obj ->
   ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
    NCic.substitution * NCic.obj)
   list * bool
 
-val disambiguate_path: CicNotationPt.term -> NCic.term
+val disambiguate_path: NotationPt.term -> NCic.term