X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.mli;h=86ede901cdaf5797afe50b50026261d2bbb3cec2;hb=93ce01455cfeba6b29e3c8a57e28f56559fb891d;hp=0e228de10ba3f37cdf19e9973e5ddd33d150eefa;hpb=3323758b99384afb5c7a70aa31bc006a78af64dd;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index 0e228de10..86ede901c 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -33,16 +33,18 @@ val disambiguate_term :
   subst:Cic.substitution ->
   ?goal:int ->
   ?initial_ugraph:CicUniv.universe_graph -> 
-  aliases:Cic.term DisambiguateTypes.environment ->
-  universe:Cic.term DisambiguateTypes.multiple_environment option ->
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
+  aliases:'alias DisambiguateTypes.Environment.t ->
+  universe:'alias list DisambiguateTypes.Environment.t option ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
     DisambiguateTypes.Environment.key ->
-    Cic.term DisambiguateTypes.codomain_item list) ->
+    'alias list) ->
   CicNotationPt.term Disambiguate.disambiguator_input ->
-  ((DisambiguateTypes.domain_item * 
-    Cic.term DisambiguateTypes.codomain_item) list *
+  ((DisambiguateTypes.domain_item * 'alias) list *
    Cic.metasenv *                  
    Cic.substitution *
    Cic.term*
@@ -50,17 +52,19 @@ val disambiguate_term :
   bool
 
 val disambiguate_obj :
-  aliases:Cic.term DisambiguateTypes.environment ->
-  universe:Cic.term DisambiguateTypes.multiple_environment option ->
-  uri:UriManager.uri option ->     (* required only for inductive types *)
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
+  aliases:'alias DisambiguateTypes.Environment.t ->
+  universe:'alias list DisambiguateTypes.Environment.t option ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
     DisambiguateTypes.Environment.key ->
-    Cic.term DisambiguateTypes.codomain_item list) ->
+    'alias list) ->
+  uri:UriManager.uri option ->     (* required only for inductive types *)
   CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
-  ((DisambiguateTypes.domain_item * 
-    Cic.term DisambiguateTypes.codomain_item) list *
+  ((DisambiguateTypes.domain_item * 'alias) list *
    Cic.metasenv *   
    Cic.substitution *
    Cic.obj *