Hello,

I see that

src_coq[:exports code]{nat}

exports to (latex export with minted)

\mint{coq}~nat~

which does not work as inline code here. The following would work,
however, with a recent minted:

\mintinline{coq}{nat}

I have two questions:
- should we support this and generate this code?
- 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?

Thanks,

Alan

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