>> - in the meantime, I created a macro that does this for latex, but it
>> does not work for html (it exports the “src_coq” string verbatim):
>> #+macro: coq @@latex:\mintinline{coq}{$1}@@@@html:src_coq[:exports code]{$1}@@
>> Why is this macro wrong?
>
> Contents of an export snippet, e.g. @@html:...@@ are not evaluated by
> the back-end. IOW this is back-end code.

I see. I think I’ll just use <code> then and skip the syntax coloring
for the moment.

Thanks,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Athmospheric CO₂ (Updated February 4, 2016, Mauna Loa Obs.): 403.08 ppm