astring (odoc.astring)