X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.mli;fp=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.mli;h=c94273804e70a1f0bdafc7409bb282dfa9f7d377;hb=154cbc049da8d8c3dd090a919a40c90eb23cc24e;hp=78fe417683e33dd6e03cce852851cfa608cf86cd;hpb=88f24d23df67d88bf98c2ca32ac0d9854f3d9b00;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index 78fe41768..c94273804 100644
--- 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 ->