modal types, generalized arrows, and core passes written in coq

[Max Bolingbroke]

On 14 March 2011 09:13, Max Bolingbroke <batterseapower at hotmail.com> wrote:
> On 13 March 2011 18:59, Adam Megacz <megacz at cs.berkeley.edu> wrote:
>> You're still using -dcoqpass, which I asked you not to use on tutorial.hs:
>>
>>  http://article.gmane.org/gmane.comp.lang.haskell.cvs.ghc/45482
>
> I'm not using it on Tutorial.hs, I'm using it on my own
> GArrows-Pow.hs, which I showed the contents of. Did you mean to say
> that -dcoqpass is broken even on trivial examples such as that one?

It does work on HelloWorld.hs, but that program is not very
interesting for me as it doesn't make use of any heterogeneous
metaprogramming. Perhaps what I am missing is that -dcoqpass doesn't
work on programs that make use of your new features?

Incidentally, the output of -dcoqpass won't compile without the
non-standard trfrac and mathpartir style files installed. Perhaps it
is worth linking to the sites where they can be obtained:
http://www.utdallas.edu/~hamlen/projects.html and
http://cristal.inria.fr/~remy/latex/

Cheers,
Max