disambiguation can use a goal as hint for the expected type

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

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index 78fe417683e33dd6e03cce852851cfa608cf86cd..c94273804e70a1f0bdafc7409bb282dfa9f7d377 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -61,8 +61,11 @@ sig
   val disambiguate_thing:
     dbd:HSql.dbd ->
     context:'context ->
-    metasenv:'metasenv ->
+    metasenv:'metasenv -> 
     initial_ugraph:'ugraph ->
+    hint: ('metasenv -> 'raw_thing -> 'raw_thing) * 
+          (('refined_thing,'metasenv) test_result -> 'ugraph ->
+              ('refined_thing,'metasenv) test_result * 'ugraph) ->
     aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
     universe:DisambiguateTypes.codomain_item list
              DisambiguateTypes.Environment.t option ->
@@ -95,7 +98,7 @@ sig
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->
     context:Cic.context ->
-    metasenv:Cic.metasenv ->
+    metasenv:Cic.metasenv -> ?goal:int ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->