X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=4b647c780541b6ff54fa72d5d5cf4e2520e32a7d;hb=649a897eeea9908ff6a438dcf6a6969894f9bd7f;hp=5d803e979025596a354179395a8487eaa1e31482;hpb=33bdd7e8c67299d34f05ac587488dd324fc6ba42;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 5d803e979..4b647c780 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -36,7 +36,7 @@ exception Ambiguous_input
 exception DisambiguationError of
  int *
  ((Stdpp.location list * string * string) list *
-  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  (DisambiguateTypes.domain_item * string) list * 
   (Stdpp.location * string) Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
@@ -86,8 +86,8 @@ let only_one_pass = ref false;;
 
 let disambiguate_thing ~aliases ~universe
   ~(f:?fresh_instances:bool ->
-      aliases:DisambiguateTypes.environment ->
-      universe:DisambiguateTypes.multiple_environment option ->
+      aliases:'term DisambiguateTypes.environment ->
+      universe:'term DisambiguateTypes.multiple_environment option ->
       'a -> 'b)
   ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
   ~(drop_aliases_and_clear_diff: 'b -> 'b)
@@ -148,12 +148,12 @@ let disambiguate_thing ~aliases ~universe
 
 type disambiguator_thing =
  { do_it :
-    'a 'b.
-    aliases:DisambiguateTypes.environment ->
-    universe:DisambiguateTypes.multiple_environment option ->
+    'a 'b 'term.
+    aliases:'term DisambiguateTypes.environment ->
+    universe:'term DisambiguateTypes.multiple_environment option ->
     f:(?fresh_instances:bool ->
-       aliases:DisambiguateTypes.environment ->
-       universe:DisambiguateTypes.multiple_environment option ->
+       aliases:'term DisambiguateTypes.environment ->
+       universe:'term DisambiguateTypes.multiple_environment option ->
        'a -> 'b * bool) ->
     drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
     drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
@@ -207,20 +207,19 @@ let drop_aliases_and_clear_diff (choices, user_asked) =
   (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
   user_asked
 
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
-  ~aliases ~universe term
+let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term
  =
   assert (fresh_instances = None);
   let f =
-    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+    Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph
   in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff term
 
-let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library  obj =
   assert (fresh_instances = None);
-  let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+  let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff obj
 
-let disambiguate_thing ~dbd = assert false 
+let disambiguate_thing ~context = assert false