- | Cic.Const (curi, _) ->
- NCic.Const (Ref.reference_of_ouri curi Ref.Def),[]
- | Cic.MutInd (curi, tyno, _) ->
- NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)),[]
- | Cic.MutConstruct (curi, tyno, consno, _) ->
- NCic.Const (Ref.reference_of_ouri curi
- (Ref.Con (tyno,consno))),[]
+ | Cic.Const (curi, ens) ->
+ aux_ens octx ctx n_fix uri ens
+ (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ | Cic.Constant (_,Some _,_,_,_) ->
+ NCic.Const (Ref.reference_of_ouri curi Ref.Def)
+ | Cic.Constant (_,None,_,_,_) ->
+ NCic.Const (Ref.reference_of_ouri curi Ref.Decl)
+ | _ -> assert false)
+ | Cic.MutInd (curi, tyno, ens) ->
+ aux_ens octx ctx n_fix uri ens
+ (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)))
+ | Cic.MutConstruct (curi, tyno, consno, ens) ->
+ aux_ens octx ctx n_fix uri ens
+ (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))