(pp_term ~pp_parens:true t3)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
- | [] -> (*assert false*) Ast.Implicit
+ | [] -> (*assert false*) Ast.Implicit `JustOne
| [term, _] when i = 1 -> term
| _ :: tl -> get_guard (pred i) tl
in
let map (params, (id,typ), body, i) =
let typ =
match typ with
- None -> Ast.Implicit
+ None -> Ast.Implicit `JustOne
| Some typ -> typ
in
sprintf "%s %s on %s: %s \\def %s"
(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)
- | Ast.Implicit -> "?"
+ | Ast.Implicit `Vector -> "?"
+ | Ast.Implicit `JustOne -> "…"
| Ast.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
in
match pp_parens, t with
| false, _
- | true, Ast.Implicit
+ | true, Ast.Implicit _
| true, Ast.Sort _
| true, Ast.Ident (_, Some [])
| true, Ast.Ident (_, None) -> t_pp
(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 ->