String converter
Plain string
Coq string
Coq string
Plain string