The Coq mailing list

[CJ Bell <siegebell AT gmail.com>]

You can also use:

Arguments append _ _ : simpl never.

The advantage over [Opaque append] is that you can still manually
unfold append while preventing simpl from doing so.

-cj

On Thu, May 8, 2014 at 11:05 AM, Marcus Ramos
<marcus.ramos AT univasf.edu.br>
 wrote:
> Dear All,
>
> When I use the "simpl" tactic in a goal, it changes a subterm of the form "c
> ++ s", with c: ascii and s: string, into "String c s" (String is a
> constructor of the type string). How can I prevent simpl from doing this?
>
> Thanks in advance,
> Marcus.