+ | A.Meta(n, l) ->
+ let local_context l =
+ box_of mathonly (A.H, false, false) []
+ ([ Mpres.Mtext ([], "[") ] @
+ (CicNotationUtil.dress (Mpres.Mtext ([], ";"))
+ (List.map
+ (function
+ | None -> Mpres.Mtext ([], "_")
+ | Some t -> aux xmlattrs mathonly xref pos prec t) l)) @
+ [ Mpres.Mtext ([], "]")])
+ in
+ let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in
+ box_of mathonly (A.H, false, false) []
+ ([Mpres.Mtext ([], "?"^string_of_int n) ]
+ @ (if l <> [] then [lctxt_maction] else []))