+let pp_argument_pattern = function
+ | CicNotationPt.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
+ | CicNotationPt.UriPattern uri -> UriManager.string_of_uri uri
+ | CicNotationPt.VarPattern name -> name
+ | CicNotationPt.ImplicitPattern -> "_"
+ | CicNotationPt.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
+ | Some Gramext.LeftA -> "left associative "
+ | Some Gramext.RightA -> "right associative "
+ | Some Gramext.NonA -> "non associative "
+ | None -> ""
+
+let pp_precedence = function
+ | Some i -> sprintf "with precedence %d " i
+ | None -> ""
+