]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/lexicon/lexiconSync.ml
metavariable context has a separator now
[helm.git] / helm / software / components / lexicon / lexiconSync.ml
index f88a79971b32919e0441a31f85bf8999840376bd..9010dfcff01cbdefb4e74f1080a230cbcae0f89e 100644 (file)
@@ -41,7 +41,7 @@ let alias_diff ~from status =
     status.LexiconEngine.aliases []
 
 let alias_diff =
- let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in
  fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
@@ -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 =