| Ast.Ident (name, Some []) | Ast.Ident (name, None)
| Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
| Ast.NRef nref -> NReference.string_of_reference nref
+ | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic
| Ast.Ident (name, Some substs)
| Ast.Uri (name, Some substs) ->
sprintf "%s \\subst [%s]" name (pp_substs substs)
| Ast.Implicit `Vector -> "?"
- | Ast.Implicit `JustOne -> "..."
+ | Ast.Implicit `JustOne -> "…"
+ | Ast.Implicit (`Tagged name) -> "?"^name
| Ast.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+ | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
sprintf "<<pretty printing of mutual definitions not implemented yet>>"
- | Ast.Theorem (flavour, name, typ, body) ->
+ | Ast.Theorem (flavour, name, typ, body,_) ->
sprintf "%s %s:\n %s\n%s"
(pp_flavour flavour)
name