The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 16/07/2013 08:33, t x a écrit :
> (as an update, here's a minimal example)
>
> https://gist.github.com/anonymous/0b02f3ad30e154515b87
>
> the issue that is not clear to me is:
>
> *) why is it not substituting?
>
> *) how do I force a substitution?

Fixpoints are reduced only when their argument is a constructor. So 
destructing your inductive object should do the trick.

Best regards,

Guillaume