- let _,height,_,_,obj = NCicEnvironment.get_checked_obj nuri in
- let spec =
- match obj with
- NCic.Constant (_,_,None,_,_) -> NReference.Decl
- | NCic.Constant (_,_,Some _,_,_) -> NReference.Def height
- | NCic.Fixpoint (is_ind,fl,_) ->
- (* CSC: bug here: name need not be the wanted name
- Solution: a real new _reference_ should arrive here *)
- (match
- HExtlib.list_index (fun (_,name',_,_,_) -> name=name') fl,is_ind
- with
- None,_ -> assert false
- | Some (i,(_,_,recno,_,_)),true-> NReference.Fix(i,recno,height)
- | Some (i,(_,_,_,_,_)),false -> NReference.CoFix i)
- | NCic.Inductive (inductive,leftno,il,_) ->
- (match
- HExtlib.list_index (fun (_,name',_,_) -> name=name') il
- with
- None ->
- let cl =
- List.concat
- (HExtlib.list_mapi (fun (_,_,_,cl) i ->
- List.map (fun t -> i,t) cl) il)
- in
- (match
- HExtlib.list_index (fun i,(_,name',_) -> name=name') cl
- with
- None -> assert false
- | Some (j,(i,_)) -> NReference.Con (i,j,leftno))
- | Some (i,_) -> NReference.Ind (inductive,i,leftno))
- in
- NCic.Const (NReference.reference_of_spec nuri spec)