X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.mli;h=3423d79214c89045a13bab2c0dcb5632c323302b;hb=9605ffc88831066a901ea4eb8e419f277662f372;hp=6f6bbd1a1b6413b2e2b50b0757d4a5e41a483d76;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
index 6f6bbd1a1..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: #NCic.status -> NotationPt.term -> NCic.term
+val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term