The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

The compute tactic is a lot more aggressive at reducing things than
simpl. I'm not aware of any tutorial, but the Coq user manual has
quite a bit about this:

simpl only does beta, iota and expands transparent constants
http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic135.

compute does "cbv beta delta iota zeta"
http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic129

On Wed, Oct 23, 2013 at 8:55 PM, Marcus Ramos 
<mvmramos AT gmail.com>
 wrote:
> Hi,
>
> Can anyone give me a link to a tutorial on the differences between "simpl"
> and "compute"? I couldn´t find that myself.
>
> Thanks,
> Marcus.