let index_obj s uri =
let obj = NCicEnvironment.get_checked_obj uri in
match obj with
- | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
- forward_infer_step s t ty
+ | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
+ let nref = NReference.reference_of_spec uri (NReference.Def d) in
+ forward_infer_step s (NCic.Const nref) ty
| _ -> s
;;