| NCic.Fixpoint _ -> []
| NCic.Inductive _ -> []
| NCic.Constant (_,_,Some _, ty, _) ->
- let ty = (* saturare *) ty in
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
[ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
| NCic.Constant (_,_,None _, ty, _) ->
- let ty = (* saturare *) ty in
+ 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