notation factored, coercion commant taking terms and not only URI

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

diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml
index 30031943d9bb1897a5fa4a2a0dc473a715b7c796..9010dfcff01cbdefb4e74f1080a230cbcae0f89e 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -83,7 +83,7 @@ let add_aliases_for_object status uri =
 let add_aliases_for_objs =
  List.fold_left
   (fun status uri ->
-    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
      add_aliases_for_object status uri obj)
  
 module OrderedId =