- Print/Set commands removed

[helm.git] / matita / components / lexicon / lexiconEngine.mli

diff --git a/matita/components/lexicon/lexiconEngine.mli b/matita/components/lexicon/lexiconEngine.mli
index 6209ce40df3765d41b1c541d621c47df2f778015..c09fc980624484f7a379ba1ede05bc7c9947f152 100644 (file)
--- a/matita/components/lexicon/lexiconEngine.mli
+++ b/matita/components/lexicon/lexiconEngine.mli
@@ -25,6 +25,7 @@
 
 val set_proof_aliases:
  #LexiconTypes.status as 'status ->
+  implicit_aliases:bool -> (* implicit ones are made explicit *)
   GrafiteAst.inclusion_mode ->
   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status