It is now possible for commands processed by grafiteEngine to either return

[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 a3a0d766e884924ce5ae9995123cb32f2a8629dc..f99535d19da9e5b7430eab6c043a7a015d8aed1a 100644 (file)
--- a/helm/software/components/lexicon/lexiconSync.ml
+++ b/helm/software/components/lexicon/lexiconSync.ml
@@ -85,11 +85,14 @@ let add_aliases_for_object status uri =
   | Cic.Variable _
   | Cic.CurrentProof _ -> assert false
   
-let add_aliases_for_objs =
- List.fold_left
-  (fun status uri ->
-    let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
-     add_aliases_for_object status uri obj)
+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 -> assert false
  
 module OrderedId = 
 struct