?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
?map_case_indty:(NotationPt.case_indtype option ->
NotationPt.case_indtype option) ->
?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
?map_case_indty:(NotationPt.case_indtype option ->
NotationPt.case_indtype option) ->