Matitaweb:

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

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli
index b63f8afaa37d54a257d547dbf4e83f149d02fa4e..3423d79214c89045a13bab2c0dcb5632c323302b 100644 (file)
--- 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