The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Mon, 1 Aug 2011 17:17:16 +0200
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> 
> By the way, just some informal stuff, there are several ways to
> simplify a term in coq, here I used an "unfold" followed by a "fold";
> it has the great advantage that you make the simplification you
> precisely want (simpl, tends to reduce all that can be reduced,
> without recursion unrolling, often leading to better terms, but in
> your case, it was an awful one), but the disadvantage that you have
> to find the good way to use it (provide the term in which you want it
> to be rewritten).
> 
> A good workaround is to build opaque, but specified functions.

Thanks, I was wondering what the general approach was in that case
actually (after having seen terms reaching to hundreds of lines after
a simpl on a fixpoint definition)!