X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconSync.mli;h=b46af6fbbaa7c28d96faa7a3306246c50c7121d7;hb=057a399c7f497cde3a09cd46505a441d2d6bacc7;hp=f19906528792262f9322fec342b670784ebc712d;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git

diff --git a/matita/components/lexicon/lexiconSync.mli b/matita/components/lexicon/lexiconSync.mli
index f19906528..b46af6fbb 100644
--- a/matita/components/lexicon/lexiconSync.mli
+++ b/matita/components/lexicon/lexiconSync.mli
@@ -24,12 +24,4 @@
  *)
 
 val add_aliases_for_objs:
- #LexiconTypes.status as 'status -> NUri.uri list -> 'status
-
-  (** perform a diff between the aliases contained in two statuses, assuming
-    * that the second one can only have more aliases than the first one
-    * @return the list of aliases that should be added to aliases of from in
-    * order to be equal to aliases of the second argument *)
-val alias_diff:
- from:#LexiconTypes.status -> #LexiconTypes.status ->
-  (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
+ #GrafiteDisambiguate.status as 'status -> NUri.uri list -> 'status