X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.mli;h=3423d79214c89045a13bab2c0dcb5632c323302b;hb=04168c737e0916ebdbcdb1457f228bef670c657b;hp=b63f8afaa37d54a257d547dbf4e83f149d02fa4e;hpb=24fc5e5485245fe879e17d46176530b688930b3b;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
index b63f8afaa..3423d7921 100644
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
@@ -29,11 +29,7 @@ val disambiguate_term :
     DisambiguateTypes.Environment.key ->
     GrafiteAst.alias_spec list) ->
   NotationPt.term Disambiguate.disambiguator_input ->
-  (NotationPt.term *
-   NCic.metasenv *                  
-   NCic.substitution *
-   NCic.term) list * 
-  bool
+  (GrafiteAst.alias_spec,NotationPt.term,NCic.metasenv,NCic.substitution,NCic.term,unit) Disambiguate.disamb_result
   
 val disambiguate_obj :
   #NCicCoercion.status ->
@@ -50,9 +46,6 @@ val disambiguate_obj :
      GrafiteAst.alias_spec list) ->
   uri:NUri.uri ->
   string * int * NotationPt.term NotationPt.obj ->
-  (NotationPt.term NotationPt.obj * 
-   NCic.metasenv *
-   NCic.substitution * NCic.obj)
-  list * bool
+  (GrafiteAst.alias_spec,NotationPt.term NotationPt.obj,NCic.metasenv,NCic.substitution,NCic.obj,unit) Disambiguate.disamb_result
 
 val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term