The Coq mailing list

[delahaye AT jurancon.inria.fr (David Delahaye)]

    Bonsoir David,

> Est-il possible de simplifier un argument d'une tactique avant de le
> filtrer de manière à ce que genre de filtre fonctionne ?
> 
>   Match ([x:nat]x=x O) With [?1=?2] -> Cut ?1=?2.

    Oui, il faut utiliser "Eval red in", où red représente les stratégies de
réductions habituelles. Par exemple, ici, on peut mettre:

    Match Eval Cbv Beta in ([x:nat]x=x O) With [?1=?2] -> Cut ?1=?2.

    Plus généralement, chaque terme peut être préfixé par "Eval red in". On
peut donc même écrire directement:

    Cut Eval Cbv Beta in ([x:nat]x=x O).

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[Computers are like air conditioners - they stop working properly when you 
open
 Windows.]