The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 10/23/2013 12:34 AM, t x wrote:
> Thanks for your patience. My previous notation is terrible and I have 
> changed it a bit.
>
> I believe https://gist.github.com/anonymous/7112657 fixes both issues 
> on line 22.
>
> Is there anything still wrong with this?

Looks right to me now, except that you haven't checked that [RExpr] has 
a type, which is what Pierre suggested before and I neglected to mention 
in my last response.  You would also need to check that (1) all the 
[Ci]s really are constructors of [T] and not just arbitrary terms (2) 
the full pattern-match is exhaustive.  There may be other "ML-level" 
sanity checks like these that I've forgotten.