Hi Thomas,
> IIUC, your goal is to export the coq source code blocks. Does the
> following, which uses :results org, do what you want? It seems to work
> for me.
It almost works. What I get upon export is an org blog, where I can see
the "#+BEGIN_SRC coq" marker. The code inside is correctly displayed, though.
> P.S. I remembered :wrap just now. This doesn't export well, though.
>
> #+call: fetchcoq2("demo.v") :wrap src coq
>
> #+results:
> #+BEGIN_src coq
> demo.v
> #+END_src
This is very nice! The fact that it does not export well seems to be a
bug. I'll report it (in a new thread). Thank you for the suggestion.
Alan
