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 375723a765101eec11ea51e0180bfc962cc25d89..86ede901cdaf5797afe50b50026261d2bbb3cec2 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -27,49 +27,46 @@ For details, see the HELM web site: http://helm.cs.unibo.it/
 val interpretate_path :
   context:Cic.name list -> CicNotationPt.term -> Cic.term
 
-module type CicDisambiguator =
-sig
-  val disambiguate_term :
-    ?fresh_instances:bool ->
-    context:Cic.context ->
-    metasenv:Cic.metasenv -> 
-    subst:Cic.substitution ->
-    ?goal:int ->
-    ?initial_ugraph:CicUniv.universe_graph -> 
-    aliases:Cic.term DisambiguateTypes.environment ->
-    universe:Cic.term DisambiguateTypes.multiple_environment 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) ->
-    CicNotationPt.term Disambiguate.disambiguator_input ->
-    ((DisambiguateTypes.domain_item * 
-      Cic.term DisambiguateTypes.codomain_item) list *
-     Cic.metasenv *                  
-     Cic.substitution *
-     Cic.term*
-     CicUniv.universe_graph) list * 
-    bool
+val disambiguate_term :
+  context:Cic.context ->
+  metasenv:Cic.metasenv -> 
+  subst:Cic.substitution ->
+  ?goal:int ->
+  ?initial_ugraph:CicUniv.universe_graph -> 
+  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 ->
+    'alias list) ->
+  CicNotationPt.term Disambiguate.disambiguator_input ->
+  ((DisambiguateTypes.domain_item * 'alias) list *
+   Cic.metasenv *                  
+   Cic.substitution *
+   Cic.term*
+   CicUniv.universe_graph) list * 
+  bool
 
-  val disambiguate_obj :
-    ?fresh_instances:bool ->
-    aliases:Cic.term DisambiguateTypes.environment ->
-    universe:Cic.term DisambiguateTypes.multiple_environment option ->
-    uri:UriManager.uri option ->     (* required only for inductive types *)
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      Cic.term DisambiguateTypes.codomain_item list) ->
-    CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
-    ((DisambiguateTypes.domain_item * 
-      Cic.term DisambiguateTypes.codomain_item) list *
-     Cic.metasenv *   
-     Cic.substitution *
-     Cic.obj *
-     CicUniv.universe_graph) list * 
-    bool
-end
-
-module Make (C : DisambiguateTypes.Callbacks) : CicDisambiguator
+val disambiguate_obj :
+  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 ->
+    'alias list) ->
+  uri:UriManager.uri option ->     (* required only for inductive types *)
+  CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
+  ((DisambiguateTypes.domain_item * 'alias) list *
+   Cic.metasenv *   
+   Cic.substitution *
+   Cic.obj *
+   CicUniv.universe_graph) list * 
+  bool