X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.mli;h=e7c6b777fda44e7a228eda88fd7825b97f775bbb;hb=6e62c12e14cea178366801f8d5e47fc6adaf1200;hp=a2cc0d0e7b04489333cadfb33572aa9b60dfbb49;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index a2cc0d0e7..e7c6b777f 100644
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/components/cic_disambiguation/disambiguate.mli
@@ -34,6 +34,8 @@ val interpretate_path :
   context:Cic.name list -> CicNotationPt.term ->
     Cic.term
 
+type 'a disambiguator_input = string * int * 'a
+    
 module type Disambiguator =
 sig
   (** @param fresh_instances when set to true fresh instances will be generated
@@ -47,7 +49,7 @@ sig
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
-    CicNotationPt.term ->
+    CicNotationPt.term disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term *
@@ -61,7 +63,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    CicNotationPt.obj ->
+    CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *