match kind with
| NCic.Fixpoint _ -> []
| NCic.Inductive _ -> []
- | NCic.Constant (_,_,_, ty, _) ->
- let ty = (* saturare *) ty in
+ | NCic.Constant (_,_,Some _, ty, _) ->
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
[ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
+ | NCic.Constant (_,_,None, ty, _) ->
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
+ [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))]
in
let status = basic_index_obj data status in
let dump = record_index_obj data :: status#dump in