The Coq mailing list

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

On 11/04/2014 18:41, Nuno Gaspar wrote:

> Example redtest:
>    5 + 3 - 1 = 9.
> Proof.
>    simpl.
>
> simpl will fully reduce the expression. What if I didn't want the minus
> function to reduce?

If you want the change to be global, you can use the following command:

  Arguments minus n m : simpl never.

Best regards,

Guillaume