X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FgrafiteDisambiguate.mli;h=401eba1152ada7565b7dfc1919dd8220c1e4ab4c;hb=f4460413546165a7fabbf1e1da4cf2f5a44b26b9;hp=6b203cab4c1241df21099359f91b97606b02426c;hpb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;p=helm.git

diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/lexicon/grafiteDisambiguate.mli
index 6b203cab4..401eba115 100644
--- a/matita/components/lexicon/grafiteDisambiguate.mli
+++ b/matita/components/lexicon/grafiteDisambiguate.mli
@@ -23,11 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-type db = {
-  aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
-  multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
-  new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
-}
+type db
 
 class type g_status =
  object
@@ -43,6 +39,10 @@ class status :
   method set_disambiguate_status: #g_status -> 'self
  end
 
+val eval_with_new_aliases:
+ #status as 'status -> ('status -> 'a) ->
+  (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a
+
 val set_proof_aliases:
  #status as 'status ->
   implicit_aliases:bool -> (* implicit ones are made explicit *)
@@ -71,3 +71,8 @@ type pattern =
 
 val disambiguate_npattern:
   GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+
+val disambiguate_cic_appl_pattern:
+ #status ->
+  NotationPt.argument_pattern list ->
+   NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern