The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Victor Porton wrote:
> Jose Grimm's GAIA inherited this mode of expressing equality for 
> propositions, as his work was based on the work of Carlos Simpson.
>
> Now there exists:
>
> Require Import Setoid.
>
> It allows rewrite to work with <->.
>
> Now we need to make a decision: Should we switch to using Setoid from standard 
> library and replace every = comparing propositions with <->?
>   

Let me just suggest that this discussion may be too specific for 
coq-club.  I don't believe many people here use that specific library.

> I'm yet weak in imperative proofs scripts as I instead decided to learn the 
> declarative proof mode.

IMO, standard Ltac proving is the technique to learn.  The declarative 
mode is much less mature and has many fewer users (I would be surprised 
if you could find 5 people on coq-club who are qualified to answer 
questions about it, compared to 100's for Ltac).