The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

> Le 29 mai 2015 à 13:47, Ralf Jung 
> <jung AT mpi-sws.org>
>  a écrit :
> 
> So far, I tried Coq 8.4 only. Have there been noticeable changes to
> simplification in Coq 8.5?

Coq 8.5 comes with a tactic called cbn that is barely a backward compatible 
in place remplacement for simpl (There is even an option SimplIsCbn so that 
any invocation of simpl calls the cbn machinery. It is not perfect and 
therefore not done by default: activating it on the standard library requires 
to modify 50 lines for example.)

It use the same syntax as lazy or cbn to allow the control constant by 
constant of which one can be unfolded while doing the « simpl » refolding 
stuff.
For example, ''cbn -[unit]'' means (more or less) apply simpl but do not 
unfold the constant unit where ''cbn [mult plus]'' means apply simpl but 
unfold only mult and plus, etc

Pierre B.