val visit_ast:
?special_k:(NotationPt.term -> NotationPt.term) ->
+ ?clear_interpretation:bool ->
?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
?map_case_indty:(NotationPt.case_indtype option ->
NotationPt.case_indtype option) ->
val strip_attributes: NotationPt.term -> NotationPt.term
(** @return the list of proper (i.e. non recursive) IdRef of a term *)
-val get_idrefs: NotationPt.term -> string list
+val get_idrefs: NotationPt.term -> (string * string option * string) list
(** generalization of List.combine to n lists *)
val ncombine: 'a list list -> 'a list list
val string_of_literal: NotationPt.literal -> string
+val html_of_literal: NotationPt.literal -> string
val dress: sep:'a -> 'a list -> 'a list
val dressn: sep:'a list -> 'a list -> 'a list