- Print/Set commands removed

[helm.git] / matita / components / lexicon / lexiconTypes.ml

diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml
index 5e6a0a326d91b51cc9c4c832a77f664c79a3f301..3aa2dadab344a166da168bcadc81bf39e1defd8a 100644 (file)
--- a/matita/components/lexicon/lexiconTypes.ml
+++ b/matita/components/lexicon/lexiconTypes.ml
@@ -27,12 +27,14 @@
 
 type lexicon_status = {
   aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
-  multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t
+  multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
+  new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
 }
 
 let initial_status = {
   aliases = DisambiguateTypes.Environment.empty;
-  multi_aliases = DisambiguateTypes.Environment.empty
+  multi_aliases = DisambiguateTypes.Environment.empty;
+  new_aliases = []
 }
 
 class type g_status =