cicNotation* ==> notation*

[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.mli

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli
index d28708e3a533565276449683e61bc6be95ad308c..25ac95ff47bffddbe9ee340f6d422c268205aff1 100644 (file)
--- 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