(String.concat " and " (List.map map definitions))
(pp_term term)
| Ast.Ident (name, Some []) | Ast.Ident (name, None)
- | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
- name
+ | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+ | Ast.NRef nref -> NReference.string_of_reference nref
| Ast.Ident (name, Some substs)
| Ast.Uri (name, Some substs) ->
sprintf "%s \\subst [%s]" name (pp_substs substs)
(List.map
(fun (name,ty,coercion,arity) ->
" " ^ name ^
- if coercion then (":" ^
- if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
- pp_term ty) fields)
-
+ (if coercion then
+ (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ")
+ else ": ") ^
+ pp_term ty)
+ fields)
+
let pp_obj pp_term = function
| Ast.Inductive (params, types) ->
let pp_constructors constructors =
let rec pp_cic_appl_pattern = function
| Ast.UriPattern uri -> UriManager.string_of_uri uri
+ | Ast.NRefPattern nref -> NReference.string_of_reference nref
| Ast.VarPattern name -> name
| Ast.ImplicitPattern -> "?"
| Ast.ApplPattern aps ->