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

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index f99535d19..616c3ef5a 100644
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -92,7 +92,20 @@ let add_aliases_for_objs status =
        (fun status uri ->
          let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
           add_aliases_for_object status uri obj) status uris
-  | `New nrefs -> assert false
+  | `New nrefs ->
+     List.fold_left
+      (fun status nref ->
+        let references = NCicLibrary.aliases_of nref in
+        let new_env =
+         List.map
+          (fun u ->
+            let name = NCicPp.r2s true u in
+             DisambiguateTypes.Id name,
+              LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+          ) references
+        in
+         LexiconEngine.set_proof_aliases status new_env
+      ) status nrefs
  
 module OrderedId = 
 struct