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

[Adam Megacz]

Adam Megacz <megacz at cs.berkeley.edu> writes:
> you've convinced me that there's no reason to have -XRebindableSyntax
> active on depth=0 terms.  So I'm going to try to find a way to have
> -XModalTypes desugar depth>0 terms as if -XRebindableSyntax were
> enabled -- that way the flag won't be necessary and won't mess with
> flat terms.

Okay, I've implemented this and checked it in -- but, as mentioned on
the webpage, what's up there isn't going to build out-of-the-box (unless
you manually merge in the last two months' worth of changes to my branch
of the base library, which isn't actually as hard as it sounds).

Anyways, -XRebindableSyntax is no longer turned on by -XModalTypes and I
do my best to simulate its effects whenever the syntactical depth is
greater than zero.  I probably missed a bunch of cases, though -- but I
will try to deal with them as they arise.

  - a