disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.mli

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index 0e228de10ba3f37cdf19e9973e5ddd33d150eefa..86ede901cdaf5797afe50b50026261d2bbb3cec2 100644 (file)
--- 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 *