- sprintf "default \"%s\" %s" what
- (String.concat " " (List.map UriManager.string_of_uri uris))
- | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
- sprintf "interpretation \"%s\" '%s %s = %s"
- dsc symbol
- (String.concat " " (List.map pp_argument_pattern arg_patterns))
- (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
- | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
- sprintf "notation %s\"%s\" %s %s for %s"
- (pp_dir_opt dir_opt)
- (pp_l1_pattern l1_pattern)
- (pp_associativity assoc)
- (pp_precedence prec)
- (pp_l2_pattern l2_pattern)
- | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m)
- | Render _
- | Dump _ -> assert false (* ZACK: debugging *)