let add_obj u obj =
storage := (u,obj)::!storage;
let _,height,_,_,obj = obj in
let references =
match obj with
NCic.Constant (_,name,None,_,_) ->
let add_obj u obj =
storage := (u,obj)::!storage;
let _,height,_,_,obj = obj in
let references =
match obj with
NCic.Constant (_,name,None,_,_) ->
| NCic.Constant (_,name,Some _,_,_) ->
| NCic.Constant (_,name,Some _,_,_) ->
| NCic.Fixpoint (is_ind,fl,_) ->
HExtlib.list_mapi
(fun (_,name,recno,_,_) i ->
if is_ind then
| 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))
| NCic.Inductive (inductive,leftno,il,_) ->
List.flatten
(HExtlib.list_mapi
(fun (_,iname,_,cl) i ->
HExtlib.list_mapi
(fun (_,cname,_) j->
| 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))
NReference.reference_of_spec u
(NReference.Ind (inductive,i,leftno))]
) il)
NReference.reference_of_spec u
(NReference.Ind (inductive,i,leftno))]
) il)