sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
definitions))
(pp_term term)
- | CicAst.Ident (name, []) -> name
- | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+ | CicAst.Ident (name, Some [])
+ | CicAst.Ident (name, None) ->
+ name
+ | CicAst.Ident (name, Some substs) -> sprintf "%s[%s]" name (pp_substs substs)
| CicAst.Implicit -> "?"
| CicAst.Meta (index, substs) ->
sprintf "%d[%s]" index