| 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 `Vector -> "…"
+ | Ast.Implicit `JustOne -> "?"
+ | Ast.Implicit (`Tagged name) -> "?"^name
| Ast.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
| Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
| Ast.Symbol (name, _) -> "'" ^ name
- | Ast.UserInput -> ""
+ | Ast.UserInput -> "%"
| Ast.Literal l -> pp_literal l
| Ast.Layout l -> pp_layout l
match pp_parens, t with
| false, _
| true, Ast.Implicit _
+ | true, Ast.UserInput
| true, Ast.Sort _
| true, Ast.Ident (_, Some [])
| true, Ast.Ident (_, None) -> t_pp
(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