X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=c82caf3371eecbeccbe7605bb4a08b6a4541c313;hb=69f03015a62c9ca2ae7d8a446540e31cc9a6e84c;hp=616c3ef5a1f3f71f6a6cdc37e21eecbbeb454518;hpb=0caee5d7da2d106650189660f4c74928a42b8b16;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index 616c3ef5a..c82caf337 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -33,7 +33,7 @@ let alias_diff ~from status =
       try
        let description2 = 
           LexiconAst.description_of_alias 
-            (Map.find domain_item from.LexiconEngine.aliases)
+            (Map.find domain_item from#lstatus.LexiconEngine.aliases)
        in
         if description1 <> description2 then
          (domain_item,codomain_item)::acc
@@ -42,13 +42,9 @@ let alias_diff ~from status =
       with
        Not_found ->
          (domain_item,codomain_item)::acc)
-    status.LexiconEngine.aliases []
+    status#lstatus.LexiconEngine.aliases []
 ;;
 
-let alias_diff =
- let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in
- fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
-
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate automatic aliases **)
 let extract_alias types uri = 
@@ -125,8 +121,8 @@ let id_list_diff l2 l1 =
 
 let time_travel ~present ~past =
   let notation_to_remove =
-    id_list_diff present.LexiconEngine.notation_ids
-     past.LexiconEngine.notation_ids
+    id_list_diff present#lstatus.LexiconEngine.notation_ids
+     past#lstatus.LexiconEngine.notation_ids
   in
    List.iter CicNotation.remove_notation notation_to_remove