X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconSync.ml;h=a3a0d766e884924ce5ae9995123cb32f2a8629dc;hb=8cfe7f6b2f82db366cf7c868e779b9b1783b637f;hp=ed243fe196c48a9ff5e7499f7bdce28ed91e0432;hpb=eb9ca860db8cb06083765f7698179f16dee5303e;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index ed243fe19..a3a0d766e 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -28,9 +28,13 @@
 let alias_diff ~from status = 
   let module Map = DisambiguateTypes.Environment in
   Map.fold
-    (fun domain_item (description1,_ as codomain_item) acc ->
+    (fun domain_item codomain_item acc ->
+      let description1 = LexiconAst.description_of_alias codomain_item in
       try
-       let description2,_ = Map.find domain_item from.LexiconEngine.aliases in
+       let description2 = 
+          LexiconAst.description_of_alias 
+            (Map.find domain_item from.LexiconEngine.aliases)
+       in
         if description1 <> description2 then
          (domain_item,codomain_item)::acc
         else
@@ -39,6 +43,7 @@ let alias_diff ~from status =
        Not_found ->
          (domain_item,codomain_item)::acc)
     status.LexiconEngine.aliases []
+;;
 
 let alias_diff =
  let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in
@@ -60,8 +65,8 @@ let extract_alias types uri =
 let build_aliases =
  List.map
   (fun (name,uri) ->
-    DisambiguateTypes.Id name,
-     (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri))
+    DisambiguateTypes.Id name, LexiconAst.Ident_alias (name, 
+     UriManager.string_of_uri uri))
 
 let add_aliases_for_inductive_def status types uri = 
   let aliases = build_aliases (extract_alias types uri) in