The Coq mailing list

[Jean-Marie Madiot <madiot AT gmail.com>]

> Sure, in this particular example I could do simpl plus, but I would like to
> be able to set this kind of "guard" for some functions, and also be able to
> unset them on demand.

for your example you can use:

  simpl (5 + 3).

or

  simpl (_ + 3).

if that is enough "guard" for you.