X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=d92b74091ab353afbd1cc692229d8907628e186b;hb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;hp=7f16fe883c0e6564707ce12679c3dd136ae6443e;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml
index 7f16fe883..d92b74091 100644
--- a/matita/components/lexicon/lexiconEngine.ml
+++ b/matita/components/lexicon/lexiconEngine.ml
@@ -37,14 +37,12 @@ type lexicon_status = {
   aliases: L.alias_spec DisambiguateTypes.Environment.t;
   multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t;
   lexicon_content_rev: LexiconMarshal.lexicon;
-  notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
 }
 
 let initial_status = {
   aliases = DisambiguateTypes.Environment.empty;
   multi_aliases = DisambiguateTypes.Environment.empty;
   lexicon_content_rev = [];
-  notation_ids = [];
 }
 
 class type g_status =
@@ -153,9 +151,7 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd =
        (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
   | _-> cmd
  in
- let sstatus,notation_ids' = CicNotation.process_notation sstatus cmd in
- let status =
-   { status with notation_ids = notation_ids' @ status.notation_ids } in
+ let sstatus = CicNotation.process_notation sstatus cmd in
  let sstatus = sstatus#set_lstatus status in
   match cmd with
   | L.Include (loc, baseuri, mode, fullpath) ->