X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.mli;h=52919dfa1f7cebc3eb38d32de51d97af37a68c2a;hb=3b4ec24b0bf7b1cd23cdc632fa3fcbb9dbbda139;hp=375723a765101eec11ea51e0180bfc962cc25d89;hpb=ad586dd2ff1080ad6d71587a07772c2596b32a96;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
index 375723a76..52919dfa1 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli
@@ -27,49 +27,48 @@ 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 ->
+  expty:Cic.term option ->
+  ?initial_ugraph:CicUniv.universe_graph -> 
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
+  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) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
+  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