The backward compatible management of aliases for NG is now fully completed.

[helm.git] / helm / software / components / ng_kernel / nCicLibrary.ml

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fa96a69b44224ff44c3642ae02d323152aa48c45..86822aa74b28f56878e4fdeffd4cb6e563178654 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -20,36 +20,45 @@ let aliases = ref [];;
 let resolve name =
  try
   HExtlib.filter_map
-   (fun (name',nref) -> if name'=name then Some nref else None) !aliases
+   (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases
  with
   Not_found -> raise (ObjectNotFound (lazy name))
 ;;
 
+let aliases_of uri =
+ try
+  HExtlib.filter_map
+   (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases
+ with
+  Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri)))
+;;
+
 let add_obj u obj =
  storage := (u,obj)::!storage;
   let _,height,_,_,obj = obj in
   let references =
    match obj with
       NCic.Constant (_,name,None,_,_) ->
-       [name,NReference.reference_of_spec u NReference.Decl]
+       [u,name,NReference.reference_of_spec u NReference.Decl]
     | NCic.Constant (_,name,Some _,_,_) ->
-       [name,NReference.reference_of_spec u (NReference.Def height)]
+       [u,name,NReference.reference_of_spec u (NReference.Def height)]
     | NCic.Fixpoint (is_ind,fl,_) ->
        HExtlib.list_mapi
         (fun (_,name,recno,_,_) i ->
           if is_ind then
-           name,NReference.reference_of_spec u (NReference.Fix(i,recno,height))
+           u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
           else
-           name,NReference.reference_of_spec u (NReference.CoFix i)) fl
+           u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
     | NCic.Inductive (inductive,leftno,il,_) ->
        List.flatten
         (HExtlib.list_mapi
          (fun (_,iname,_,cl) i ->
            HExtlib.list_mapi
             (fun (_,cname,_) j->
-              cname,NReference.reference_of_spec u (NReference.Con (i,j,leftno))
+              u,cname,
+               NReference.reference_of_spec u (NReference.Con (i,j,leftno))
             ) cl @
-           [iname,
+           [u,iname,
              NReference.reference_of_spec u
               (NReference.Ind (inductive,i,leftno))]
          ) il)