X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=322279769fe453cc15dafb3852567e917dae91e9;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=ce9f5648214477e1c1ed2051821b3aefb9af32f5;hpb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;p=helm.git

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index ce9f56482..322279769 100644
--- a/matita/components/lexicon/lexiconSync.ml
+++ b/matita/components/lexicon/lexiconSync.ml
@@ -29,11 +29,11 @@ let alias_diff ~from status =
   let module Map = DisambiguateTypes.Environment in
   Map.fold
     (fun domain_item codomain_item acc ->
-      let description1 = LexiconAst.description_of_alias codomain_item in
+      let description1 = GrafiteAst.description_of_alias codomain_item in
       try
        let description2 = 
-          LexiconAst.description_of_alias 
-            (Map.find domain_item from#lstatus.LexiconEngine.aliases)
+          GrafiteAst.description_of_alias 
+            (Map.find domain_item from#lstatus.LexiconTypes.aliases)
        in
         if description1 <> description2 then
          (domain_item,codomain_item)::acc
@@ -42,7 +42,7 @@ let alias_diff ~from status =
       with
        Not_found ->
          (domain_item,codomain_item)::acc)
-    status#lstatus.LexiconEngine.aliases []
+    status#lstatus.LexiconTypes.aliases []
 ;;
 
 let add_aliases_for_objs status =
@@ -54,8 +54,8 @@ let add_aliases_for_objs status =
       (fun u ->
         let name = NCicPp.r2s true u in
          DisambiguateTypes.Id name,
-          LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+          GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
       ) references
     in
-     LexiconEngine.set_proof_aliases status new_env
+     LexiconEngine.set_proof_aliases status GrafiteAst.WithPreferences new_env
   ) status