X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=e2d800157dd4d57c4f44852dd6735b6dfc6ebd0e;hb=25cf2297c8d14c14cfb2ff7695c9b6331825f4c9;hp=fa96a69b44224ff44c3642ae02d323152aa48c45;hpb=e02c6eaf8d50025c3be8bbf6988ab8b2a37b40da;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fa96a69b4..e2d800157 100644
--- 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+1,leftno))
             ) cl @
-           [iname,
+           [u,iname,
              NReference.reference_of_spec u
               (NReference.Ind (inductive,i,leftno))]
          ) il)