The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

In the follow code example:

https://gist.github.com/anonymous/6336486

How do I rewrite extract_valueT as extract_valueT' through the use of match?

In particular, I don't know how to use the "rewrite H" for the types.

(I prefer style 2 as it's easier to read, even if a bit more involved to write.)

Thanks!