The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 16 jun 2005, Devisschere Yann wrote:

> rules. Is there an order, according to the "hint rewrite ..." or does
> autorewrite try to use the more specific rewriting rule or the more
> general ?
> 
> I don't find explanations of that neither in Coq'art nor in the Coq
> reference manual. (all the examples use specific excluding rules)

As far as I know, autorewrite is almost equivalent to : 

repeat progress (try rewrite R1 ; try rewrite R2 ; try rewrite R3 ...).

where Ri's are the lemmas in the database. I don't know the order in which
lemmas are used, but there is no other strategy.

Cheers,

Pierre.

> 
> Please help me.
> Thanks.
> 
> (Hoping this tiny example is enough clear and representative of my whole
> problem.)
> 
> Yann Devisschere