let rec pp rels =
function
NCic.Rel i -> List.nth rels (i - 1)
- | NCic.Const _ as t ->
- NotationPt.Ident
- (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+ | NCic.Const _ as t -> NotationPt.NCic t
| NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
| NCic.Meta _
| NCic.Implicit _ -> assert false