The Coq mailing list

[t x <txrev319 AT gmail.com>]

I'm trying to understand how to change functions from ": option X" to ": X" by passing along proofs.

However, in this example:

https://gist.github.com/anonymous/9f56cd467bc2e80c7d9c#file-test-v-L45

I get a stack overflow when I try to process lines 45-49. (Weirdly enough, if I change line 47 to:

| nil => fun H => _

then everything goes through fine.

What am I doing wrong?