disambiguation can use a goal as hint for the expected type

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguator.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index f83225c35d411203282d1bab13bf35877cfb5aeb..360d56f0285caf875a59defe370be8a8e1ae085c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -207,12 +207,12 @@ let drop_aliases_and_clear_diff (choices, user_asked) =
   (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
   user_asked
 
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?goal ?initial_ugraph
   ~aliases ~universe term
  =
   assert (fresh_instances = None);
   let f =
-    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?goal ?initial_ugraph
   in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff term