+let pp_argument_pattern = function
+ | Ast.IdentArg (eta_depth, name) ->
+ let eta_buf = Buffer.create 5 in
+ for i = 1 to eta_depth do
+ Buffer.add_string eta_buf "\\eta."
+ done;
+ sprintf "%s%s" (Buffer.contents eta_buf) name
+
+let rec pp_cic_appl_pattern = function
+ | Ast.UriPattern uri -> UriManager.string_of_uri uri
+ | Ast.VarPattern name -> name
+ | Ast.ImplicitPattern -> "_"
+ | Ast.ApplPattern aps ->
+ sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))
+
+let pp_l1_pattern = CicNotationPp.pp_term
+let pp_l2_pattern = CicNotationPp.pp_term
+
+let pp_associativity = function
+ | Gramext.LeftA -> "left associative"
+ | Gramext.RightA -> "right associative"
+ | Gramext.NonA -> "non associative"
+
+let pp_precedence i = sprintf "with precedence %d" i
+
+let pp_dir_opt = function
+ | None -> ""
+ | Some `LeftToRight -> "> "
+ | Some `RightToLeft -> "< "
+
+let pp_metadata =
+ function
+ | Dependency buri -> sprintf "dependency %s" buri
+ | Baseuri buri -> sprintf "baseuri %s" buri
+