(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.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
- (List.map (function None -> "_" | Some t -> pp_term t) substs))
+ (List.map (function None -> "?" | Some t -> pp_term t) substs))
| Ast.Num (num, _) -> num
| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
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.ImplicitPattern -> "?"
| Ast.ApplPattern aps ->
sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))