Bug fixed: pretty-printing of aliases when the OK button is pressed in the

[helm.git] / helm / software / components / lexicon / disambiguatePp.mli

diff --git a/helm/software/components/lexicon/disambiguatePp.mli b/helm/software/components/lexicon/disambiguatePp.mli
index e85a284437cd385b11747f31ba8611da3c7193ee..c41bf6d78b1dd21a654596767d498ddc5cb4d433 100644 (file)
--- a/helm/software/components/lexicon/disambiguatePp.mli
+++ b/helm/software/components/lexicon/disambiguatePp.mli
@@ -23,9 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-val aliases_of_domain_and_codomain_items_list:
-  (DisambiguateTypes.domain_item * 
-   Cic.term DisambiguateTypes.codomain_item) list ->
-    LexiconAst.alias_spec list
+val alias_of_domain_and_desc:
+  DisambiguateTypes.domain_item -> string -> LexiconAst.alias_spec
 
 val pp_environment: Cic.term DisambiguateTypes.environment -> string