- cic_exportation, cic_acic, acic_content (only parts related to acic)

[helm.git] / matita / components / lexicon / lexiconSync.ml

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index c82caf3371eecbeccbe7605bb4a08b6a4541c313..325a8d8375ac392cfea04c1de76ac324b3c7dca8 100644 (file)
--- a/matita/components/lexicon/lexiconSync.ml
+++ b/matita/components/lexicon/lexiconSync.ml
@@ -82,13 +82,9 @@ let add_aliases_for_object status uri =
   | Cic.CurrentProof _ -> assert false
   
 let add_aliases_for_objs status =
- function
-    `Old uris ->
-      List.fold_left
-       (fun status uri ->
-         let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
-          add_aliases_for_object status uri obj) status uris
-  | `New nrefs ->
+  function
+   `Old _ -> assert false (* MATITA 1.0 *)
+ | `New nrefs ->
      List.fold_left
       (fun status nref ->
         let references = NCicLibrary.aliases_of nref in